mod QQ is
    inc ALLRULES .
    inc ALLOPS .
****    inc MODEL-CHECKER .
***(
  sort State .
  subsort Dish < State .
)
***********************************
sort Contents .
subsort Contents < Soup .

op CLoContents : -> Contents .
eq CLoContents = empty .

op CLmContents : -> Contents .
eq CLmContents = EgfR .

op CLiContents : -> Contents .
eq CLiContents = [Hras - GDP] .

op CLcContents : -> Contents .
eq CLcContents =  Pi3k Gabs Sos1 .

op NUcContents : -> Contents .
eq NUcContents = empty .

op RNACContents : -> Contents .
eq RNACContents = empty .

op DNACContents : -> Contents .
eq DNACContents = empty .

op tinyDish : -> Dish .
eq tinyDish = PD(
**** [Cell |    
{XOut  | Egf}
{CLm  | CLmContents }
{CLi   | CLiContents}
{CLc   | CLcContents}
**** ]
) .

**** op allDish : -> Dish .
**** eq allDish = tinyDish .

endm

***********************************
