Maude-help mailing list

[Wilson Castro <castro AT informatik.uni-kl.de>]

Hi Paco,

I was to erased this comment of line 124 in full-maude.maude and changed all 
content of model=checker.maude file, as you was explainted to Alexandre. But 
have follow error, when I will the last object modul from this sample.

He descomentado la linea 124 en full-maude.maude y cambiado todo el contenido 
del archivo  model-checker.maude como está en la respuesta que das a 
Alexandre pero obtengo el siguente error al compilar el último modulo de este 
ejemplo.

----------------------- 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.



Gruss,
-- 
Wilson Castro
AG Grundlagen der Informatik
Promotionsprogramm Student
34/423
0631-2052155 
Fachbereich Informatik
castro AT informatik.uni-kl.de