Maude-help mailing list

[Jon Haugsand <jonhaug AT ifi.uio.no>]

I have read the maude manual's chapter on model checking.  However,
the explanations cannot directly be used in full maude as I cannot see
how to use modules like MYCLASSES-PRED and such.  Therefore I have the
following fragments in my omod specification:

(omod IA is

  protecting BOOL-ALG .
  protecting DATA .
  protecting NAT .
  protecting STRING .
  protecting CHOOSE .
  
  including MODEL-CHECKER .
  including LTL-SIMPLIFIER .
  including SATISFACTION .
...

  subsort Configuration < State .
  op isChecked : Nat -> Prop .
  op countAt : Nat -> Prop .
...
endom)

That is, I mix the omod rewrite modules with the predicate
specifications.  However, this does not seem to work:

   Maude> (red modelCheck(initAll2, <> countAt(2)) .)
   Process Maude segmentation fault

This happens after a few seconds of run time.  Is there something I
have done that clearly should be done differently, or do I have to
dissect my (too long and too involved) specification to find out?

-- 
Jon Haugsand
  Dept. of Informatics, Univ. of Oslo, Norway, 
mailto:jonhaug AT ifi.uio.no
  http://www.ifi.uio.no/~jonhaug/, Phone: +47 22 85 24 92