Maude-help mailing list

[Eugen-Ioan Goriac <egoriac AT info.uaic.ro>]

Hello,

I was wondering if I could check a model for deadlocks using the 
provided model-checker(.maude). It's clear that this can be done using 
the search command (as shown in a simple example below), but is there a 
way to do it using > red modelCheck(initial, ...) . ?

mod TESTER is
 including SATISFACTION .
 including LTL-SIMPLIFIER .
 including MODEL-CHECKER .
 including INT .

 ops a b c : -> State .
 rl [nexta] : a => b .
 rl [nextb] : b => c .
 --- rl [nextc] : c => a . --- this rule frees the system from deadlocks

 op initial : -> State .
 eq initial = b . 
endm

> search in TESTER : initial =>! S:State .

I'm asking this question because there is a deadlock constant of sort 
RuleName in the source of the model-checker, but unfortunately I can't 
find anything about it in the manual.

Thank you very much for your time,
Eugen