Maude-help mailing list

[Steven Eker <eker AT csl.sri.com>]

The fact that you are seeing a segmentation fault rather than an internal 
error means you have a stack overflow. This could be caused by runaway 
recursion or model checking a model that is infinite or just to big for the 
amount of stack space allowed (the model checker uses double depth-first 
search to look for counter examples). You could try "unlimit stacksize" or 
whatever the equivalent command is for your shell.

Steven

On Thursday 23 June 2005 07:31, Jon Haugsand wrote:
> 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?