Maude-help mailing list

[Francisco Duran <duran AT lcc.uma.es>]

Wilson,

I'm working on a new version of Full Maude in which the model cheker is used in 
a more convenient way.

Now, any module loaded in Core Maude can be used in Full Maude. To do so,
one must use the (new) Full Maude 'load' command. The load command
takes the _name_of_the_module_ to be loaded as argument, and results
in the insertion of such a module and all its submodules into
Full Maude's database. This may be particularly useful in the case
of using the model checker. When loading the specification of Full Maude, the 
model-checker.maude file is loaded, so want can now do e.g.

   (load MODEL-CHECKER .)

   (mod CHECK-RESP is
      protecting MODEL-CHECKER .
      ...
    endm)

   (red p(0) |= (<> Qstate) .)

I'm sending to you in a separate email the under-development version of Full 
Maude on which you can run a modified version of the spec you sent me (look for 
my comments on it).

Best regards,

Paco Duran


Wilson Castro wrote:

> Hello,
>
> I was to erased this comment of line 124 in full-maude.maude and changed all 
> content of model=checker.maude file, as Francisco Duran was explainted to 
> Alexandre in mailing list . But I have follow error, when I will the last 
> object modul from this sample.
>
> ----------------------- Begin SAMPLE --------------------------------
> *** Token Ring architecture of n processes
> *** n is a parameter
>
> *** PROPERTIES
> ****** mutual exclusion: 
> ****** each process passing on token to the next process in the ring 
> ****** when it is done using the shared resource.
>
> (fth NZNAT* is
>   protecting NAT .
>   op * : -> NzNat .
> endfth)
>
> *** Nat mod *
> (fmod NAT/(X :: NZNAT*) is
>   sort Nat/(X) .
>
>   op `[_`] : Nat -> Nat/(X) .
>   op _+_ : Nat/(X) Nat/(X) -> Nat/(X) .
>   op _*_ : Nat/(X) Nat/(X) -> Nat/(X) .
>   
>   vars N M : Nat .
>   ceq [N] = [N rem *] if N >= * .
>   eq [N] + [M] = [N + M] . 
>   eq [N] * [M] = [N * M] . 
> endfm)
>
> *** TOKEN RING module parameterized by n
> *** To beginning in the init state.
> *** 1. mutual exclusion: never two process in crit mod simultaneously
> *** 2. guaranteed: 
> ****** each P reaches its critical section, and
> ****** it does so again after 2*n steps
> (omod TOK-RING (X :: NZNAT*) is protecting NAT/(X) .
>   sort Mode .
>   subsort Nat/(X) < Oid .
>   ops wait crit : -> Mode .
>   msg tok : Nat/(X) -> Msg .
>   op init : -> Configuration .
>   op make-init : Nat/(X) -> Configuration .
>   
>   class Proc | mode : Mode .
>   var N : Nat .
>   
>   ceq init = tok([0]) make-init([N]) if s(N) := * .
>   ceq make-init([s(N)]) = <[s(N)] : Proc | mode : wait > make-init([N]) if N < 
> * .
>   eq make-init([0]) = <[0] : Proc | mode : wait > .
>   
>   rl [enter] : tok([N]) < [N] : Proc | mode : wait >
>     => < [N] : Proc | mode : crit > .
>   
>   rl [exit] : < [N] : Proc | mode : crit >
>     => < [N] : Proc | mode : wait > tok([s(N)]) .
> endom)
>
> *** for each property there is a different formula for each n
>
> (omod CHECK-TOK-RING(X :: NZNAT*) is
>   inc TOK-RING(X) .
>   inc MODEL-CHECKER .
>   subsort Configuration < State .
>   
>   op inCrit : Nat/(X) -> Prop .
>   op twoInCrit : -> Prop .
>   
>   var N : Nat .
>   vars A B : Nat/(X) .
>   var C : Configuration .
>   var F : Formula .
>
>   eq < A : Proc | mode : crit > C |= inCrit(A) = true .
>   eq < A : Proc | mode : crit > < B : Proc | mode : crit > C |= twoInCrit = 
> true .
>
>   op guaranteedReentrance : -> Formula .
>   op allProcessesReenter : Nat -> Formula .
>   op nextIter_ : Formula -> Formula .
>   op nextIterAux : Nat Formula -> Formula .
>   
>   ceq guaranteedReentrance = allProcessesReenter(N) if s(N) := * .
>   
>   eq allProcessesReenter(s(N)) 
>     = (<> inCrit([s(N)])) /\
>        [] (inCrit(s[N]) -> (nextIter inCrit([s(N)]))) /\ 
> allProcessesReenter(N) .
>   
>   eq allProcessesReenter(0) = (<> inCrit([0])) /\ 
>        [] (inCrit([0]) -> (nextIter inCrit([0]))) .
>   
>   eq nextIter F = nextIterAux(2 * *, F) .  
>   eq nextIterAux(s N, F) = 0 nextIterAux(N, F) .  
>   eq nextIterAux(0, F) =  F .  
>
> endom)
>
> *** For n = 5
>
> (view 5 from NZNAT* to NAT is
>   op * to term 5 . 
> endv)
>
> (red in CHECK-TOK-RING(5) : init |= [] ~ twoIntCrit .)
>
> ---------------------------- end sample1.maude -------------------------
>
>
>
> =============== errors ====================
> Maude> load full-maude.maude
> Warning: no loop state.
> Warning: no loop state.
>
>                Full Maude 2.1.1 (July 20th, 2004)
>
> Maude> load sample1.maude
> rewrites: 1091 in 86ms cpu (101ms real) (12542 rewrites/second)
> Introduced theory NZNAT*
>
> rewrites: 3224 in 15ms cpu (28ms real) (201525 rewrites/second)
> Introduced module NAT/
>
> rewrites: 7532 in 37ms cpu (50ms real) (198241 rewrites/second)
> Introduced module TOK-RING
>
> rewrites: 5254 in 23ms cpu (34ms real) (218953 rewrites/second)
> Error: Module MODEL-CHECKER not in database.
> Introduced module CHECK-TOK-RING
>
> rewrites: 309 in 9ms cpu (31ms real) (30906 rewrites/second)
> Introduced view 5
>
> rewrites: 879 in 5ms cpu (4ms real) (175800 rewrites/second)
> Error: Module CHECK-TOK-RING not compiled.
>
>
>
>
> Thank you very much.