***(

 Brands & Chaum process specification

(Verifier) : 

−(Commit@t1) · 
+(n(V?,f1)@t2) ·
−((n(V?, f1) ⊕ NP )@t3) ·
if t3−t2 ≤ 2*d 
then −(SP @t4) · 
     if open(NP,SP,Commit) then −(sign(P,n(V?,f1);NP ⊕ n(V?,f1))@t5) 
     else nilP
else nilP

(Prover) :

+(commit(n(P?,f1),s(P?,f2))@t1) · 
−(NV @t2) ·
+((NV ⊕ n(P?,f1))@t3) · 
+(s(P?,f2)@t4) ·
+(sign(P?, NV ; n(P?, f2) ⊕ NV )@t5)


  )***

fmod PROTOCOL-EXAMPLE-SYMBOLS is
  --- Importing sorts Msg, Fresh, Public, and GhostData
  protecting DEFINITION-PROTOCOL-RULES .
  
  ----------------------------------------------------------
  --- Overwrite this module with the syntax of your protocol
  --- Notes:
  --- * Sort Msg and Fresh are special and imported
  --- * Every sort must be a subsort of Msg
  --- * No sort can be a supersort of Msg
  ----------------------------------------------------------

  --- Sort Information 
  sorts Name Nonce Honest Intruder Secret Key TMsg NTMsg TimeInfo NameTime NameTimeSet NNSet .
  subsort Nonce Key Secret < NTMsg . 
  subsort TMsg NTMsg Real < Msg .
  subsort Name < Key .
  subsort Name < Public .
  subsort Honest Intruder < Name .
  subsort NameTime < NameTimeSet .
  --- XOR ---
  subsort NNSet < NTMsg .
  subsort Nonce < NNSet .

  --- Nonce operator
  op n : Name Fresh -> Nonce [frozen] .

  --- Secret operator
  op s : Name Fresh -> Secret [frozen] .

  op sign : Name NTMsg -> NTMsg .
  op _;_ : NTMsg  NTMsg  -> NTMsg [gather (e E) frozen] .
  op commit : Nonce Secret -> NTMsg .
  op open : Nonce Secret NTMsg -> NTMsg .
  ---op sign : Name NTMsg -> NTMsg .
  op yes : -> NTMsg .
  
  --- Principals
  
  ops a b : -> Honest .
  op i : -> Intruder .

  --- Time messages
  op _@_ : NTMsg TimeInfo -> TMsg [metadata "grammar-arg-1" prec 50 format (d nis d d)] .

  --- Time information
  op _:_ : Name Real -> NameTime [prec 10] .
  
  op mt : -> NameTimeSet .
  op _#_ : NameTimeSet NameTimeSet -> NameTimeSet [assoc comm id: mt prec 20] .
  op _->_ : NameTime NameTimeSet -> TimeInfo .

  --- Distance
  op d : Name Name -> Real [comm] .
  

  --- Exclusive or
  op _*_ : NNSet NNSet -> NNSet [assoc comm frozen] .
  op null : -> NNSet .

endfm

fmod PROTOCOL-EXAMPLE-ALGEBRAIC is
  protecting PROTOCOL-EXAMPLE-SYMBOLS .
  
  ----------------------------------------------------------
  --- Overwrite this module with the algebraic properties 
  --- of your protocol
  ----------------------------------------------------------

  eq d(A:Name,A:Name) = 0/1 . 

  *** Exclusive or properties
  vars XN YN : NNSet .
  eq XN * XN = null    [variant] .
  eq XN * XN * YN = YN [variant] .
  eq XN * null = XN    [variant] .

  *** Open commitment
  eq open(N1:Nonce,Sr:Secret,commit(N1:Nonce,Sr:Secret)) = yes [variant] . 


endfm

fmod PROTOCOL-SPECIFICATION is
  protecting PROTOCOL-EXAMPLE-SYMBOLS .
  protecting DEFINITION-PROTOCOL-RULES .
  protecting DEFINITION-CONSTRAINTS-INPUT .

  ----------------------------------------------------------
  --- Overwrite this module with the strands 
  --- of your protocol
  ----------------------------------------------------------
  
  var Ke : Key .
  vars X Y Z Commit : NTMsg .
  vars r r' r1 r2 : Fresh .
  vars AB AB1 AB2 : Honest .
  vars A B : Name .
  var I : Intruder .
  vars C C1 C2 C3 C4 C5 : Name .
  vars N NA NB N1 N2 N3 N4 : Nonce .
  vars SA SB S1 S2 Sr : Secret .
  var Key : Nonce .
  vars t0 t1 t2 t3 t4 t5 t6 tx t7 t8 t9 t10 t11 t12 t13 : Real .
  vars XN YN : NNSet .
  vars d t0' t1' t2' t3' t4' t5' t6' t7' t8' t9' t10' t11' t12' t13' : Real .
  vars t0'' t1'' t2'' t3'' t4'' t5'' t6'' t7'' t8'' t9'' : Real .
  vars I1 I2 I3 I4 I5 : Real .
  vars AS1 AS2 AS3 AS4 AS5 : NameTimeSet .

  eq STRANDS-DOLEVYAO
   = :: nil :: [ nil | -(X @ AB1 : t1 -> AS1 # i : t2), --- Forward from honest participants
                        (t2 === t1 +=+ d(AB1,i) and d(AB1,i) >= 0/1),
                       +(X @ i : t2 -> AB2 : t3), nil ] & 
     :: nil :: [ nil | +(null @ i : t1 -> AS1), nil ] &
     :: r ::   [ nil | +(n(i,r) @ i : t1 -> AS1), nil ] &
     :: nil :: [ nil | -(X @ C1 : t1 -> AS1 # i : t2), (t2 === t1 +=+ d(C1,i) and d(C1,i) >= 0/1),
                       -(Y @ C2 : t3 -> AS2 # i : t4), (t4 === t3 +=+ d(C2,i) and d(C2,i) >= 0/1),
                       (t5 >= t2 and t5 >= t4),
                       +((X ; Y) @ i : t5 -> AS3), nil ] &
     :: nil :: [ nil | -(X ; Y @ C1 : t1 -> AS1 # i : t2), (t2 === t1 +=+ d(C1,i) and d(C1,i) >= 0/1),
                       +(X @ i : t2 -> AS3), nil ] &
     :: nil :: [ nil | -(X ; Y @ C1 : t1 -> AS1 # i : t2), (t2 === t1 +=+ d(C1,i) and d(C1,i) >= 0/1),
                       +(Y @ i : t2 -> AS3), nil ] &                   
     :: nil :: [ nil | -(N1 @ C1 : t1 -> AS1 # i : t2), (t2 === t1 +=+ d(C1,i) and d(C1,i) >= 0/1),
                       -(S2 @ C2 : t3 -> AS2 # i : t4), (t4 === t3 +=+ d(C2,i) and d(C2,i) >= 0/1),
                       (t5 >= t2 and t5 >= t4),
                       +(commit(N1,S2) @ i : t5 -> AS3), nil ] &
     :: nil :: [ nil | -(X @ C1 : t1 -> AS1 # i : t2), (t2 === t1 +=+ d(C1,i) and d(C1,i) >= 0/1),
                       -(N @ C2 : t3 -> AS2 # i : t4), (t4 === t3 +=+ d(C2,i) and d(C2,i) >= 0/1),
                       -(SB @ C3 : t5 -> AS3 # i : t6), (t6 === t5 +=+ d(C3,i) and d(C3,i) >= 0/1),
                       (t7 >= t2 and t7 >= t4 and t7 >= t6),
                       +(open(N,SB,X) @ i : t7 -> AS4), nil ] &
     :: nil :: [ nil | -(SB @ C1 : t1 -> AS1 # i : t2), (t2 === t1 +=+ d(C1,i) and d(C1,i) >= 0/1),
                       +(SB @ i : t2 -> AB : t3), nil ] &                   
     :: nil :: [ nil | -(X @ C1 : t1 -> AS1 # i : t2), (t2 === t1 +=+ d(C1,i) and d(C1,i) >= 0/1),
                       +(sign(i,X) @ i : t2 -> AS3), nil ] &
     :: nil :: [ nil | +(C @ i : t1 -> AS1), nil ] 
  [nonexec] .

  eq STRANDS-PROTOCOL
   = :: r :: ---Alice --- Verifier
     [ nil | -(Commit                          @ C1 : t1 -> AS1 # A : t2), ((t2 === t1 +=+ d(C1,A)) and d(C1,A) > 0/1),
             +(n(A,r)                          @ A : t2 -> AS2),
             -(n(A,r) * NB                     @ C3 : t3 -> AS2 # A : t4), (t3 >= t2 and (t4 === t3 +=+ d(C3,A)) and d(C3,A) > 0/1),
                                                 ((t4 -=- t2) <= (2/1 *=* d) and d > 0/1),
             -(SB                              @ C4 : t5 -> AS3 # A : t6), ((t6 ===  t5 +=+ d(C4,A)) and d(C4,A) > 0/1),
              (open(NB,SB,Commit) eq yes),
             -(sign(B,(n(A,r) * NB) ; n(A,r))  @ C5 : t7 -> AS4 # A : t8), ((t8 ===  t7 +=+ d(C5,A)) and d(C5,A) > 0/1),
      nil ]
     &
     :: r1,r2 :: ---Bob  --- Prover
     [ nil | +(commit(n(B,r1),s(B,r2))         @ B : t1 -> AS1),
             -(NA                              @ C1 : t2 -> AS1 # B : t3),
                                                 ((t3 === t2 +=+ d(C1,B)) and d(C1,B) > 0/1),
             +(NA * n(B,r1)                   @ B : t3 -> AS2), 
             +(s(B,r2)                         @ B : t3 -> AS3), 
             +(sign(B,(NA * n(B,r1)) ; NA)    @ B : t4 -> AS4), nil ]
  [nonexec] .

eq ATTACK-STATE(1) ---  Mafia fraud
   = :: r :: ---Alice --- Verifier
     [ nil, -(commit(n(b,r1),s(b,r2))
               @ i : t1 -> a : t2),
             ((t2 === t1 +=+ d(i,a)) and d(i,a) > 0/1),
             +(n(a,r)
               @ a : t2 -> i : t2''),
             -(n(a,r) * n(b,r1)
               @ i : t3 -> a : t4),
             (t3 >= t2 and (t4 === t3 +=+ d(i,a)) and d(i,a) > 0/1),
             ((t4 -=- t2) <= (2/1 *=* d) and d > 0/1) | nil ]
     &
     :: r1,r2 :: ---Bob  --- Prover
     [ nil,  +(commit(n(b,r1),s(b,r2))
              @ b : t1' -> i : t1''),
             -(n(a,r)
              @ i : t2'' -> b : t3'),
             ((t3' === t2'' +=+ d(i,b)) and d(i,b) > 0/1),
             +(n(a,r) * n(b,r1)
              @ b : t3' -> i : t3'') | nil ]
     || smt((d(a,i) +=+ d(b,i)) > d)
     || nil
     || nil
     || nil 
  [nonexec] .
***(
maude maude-npa.maude brands-chaum.maude 
         \||||||||||||||||||/
       --- Welcome to Maude ---
         /||||||||||||||||||\
       Maude 3.1 built: Oct 12 2020 20:12:31
       Copyright 1997-2020 SRI International
       Fri Oct 23 11:24:52 2020

      Maude-NPA Version: 3.1.5 (August 9th 2020)
      with direct composition, irreducibility constraints and time
      (To be run with Maude 3.0 or above)
      Copyright (c) 2020, University of Illinois
      All rights reserved.

 Commands:
 red unification? .           returns the unification algorithm to be used
 red new-strands? .           returns the actual protocol strands
 red displayGrammars .        for generating grammars
 red run(X,Y).                for Y backwards analysis steps for attack pattern X
 red debug(X,Y).              more information than run command
 red digest(X,Y).             less information than run command
 red summary(X,Y).            for summary of analysis steps
 red ids(X,Y).                for set of state ids
 red initials(X,Y).           for showing only initial steps
==========================================
reduce in MAUDE-NPA : displayGrammars .
rewrites: 2248900 in 3012ms cpu (3009ms real) (746646 rewrites/second)
result GrammarList: (
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl #0:NNSet notInI,
   (#0:NNSet notLeq n(#1:Name, #2:Fresh)),
   #0:NNSet notLeq #3:Nonce * n(#4:Name, #5:Fresh) => (#6:NNSet * #0:NNSet) inL .  ; 
grl (#1:NNSet * #0:NNSet) notInI,
   (#1:NNSet notLeq n(#2:Name, #3:Fresh)),
   (#1:NNSet * #0:NNSet) notLeq #4:Nonce * n(#5:Name, #6:Fresh) => #1:NNSet inL . )
| (
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl (#1:NNSet * #0:NNSet) notLeq #2:Nonce * n(#3:Name, #4:Fresh) => (#1:NNSet * #0:NNSet) inL . )
| (
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl #0:NTMsg notInI => (#0:NTMsg ; #1:NTMsg) inL . )
| (
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl #0:NTMsg notInI => (#1:NTMsg ; #0:NTMsg) inL . )
| (
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl #0:Nonce notInI,
   #0:Nonce notLeq n(#1:Name, #2:Fresh) => commit(#0:Nonce, #3:Secret) inL . )
| (
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl #0:Secret notInI,
   #0:Secret notLeq s(#1:Name, #2:Fresh) => commit(#3:Nonce, #0:Secret) inL . )
| 
grl empty => d(#1:Name, #2:Name) inL . 
| (
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl #0:Nonce notInI => open(#0:Nonce, #1:Secret, #2:NTMsg) inL . )
| (
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl #0:Secret notInI => open(#1:Nonce, #0:Secret, #2:NTMsg) inL . )
| (
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl #0:NTMsg notInI => open(#1:Nonce, #2:Secret, #0:NTMsg) inL . )
| (
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl #0:NTMsg notInI,
   (#0:NTMsg notLeq null ; n(#1:Name, #2:Fresh)),
   #0:NTMsg notLeq (#3:Nonce * n(#4:Name, #5:Fresh)) ; #3:Nonce => sign(#6:Name, #0:NTMsg) inL . )
| 
grl #0:NTMsg inL => (#1:NTMsg ; #0:NTMsg) inL .  ; 
grl #0:NTMsg inL => (#0:NTMsg ; #1:NTMsg) inL .  ; 
grl (sign(#0:Name, #1:NTMsg) notLeq sign(i, #2:NTMsg)),
   (sign(#0:Name, #1:NTMsg) notLeq sign(#3:Name, null ; n(#3:Name, #4:Fresh))),
   sign(#0:Name, #1:NTMsg) notLeq sign(#5:Name, (#6:Nonce * n(#5:Name, #7:Fresh)) ; #6:Nonce) =>
    sign(#0:Name, #1:NTMsg) inL . 
==========================================
reduce in MAUDE-NPA : summary(1, 0) .
rewrites: 8687 in 84ms cpu (85ms real) (103416 rewrites/second)
result Summary: States>> 1 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(1, 1) .
rewrites: 432248 in 620ms cpu (619ms real) (697174 rewrites/second)
result Summary: States>> 2 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(1, 2) .
rewrites: 750426 in 1352ms cpu (1351ms real) (555048 rewrites/second)
result Summary: States>> 3 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(1, 3) .
rewrites: 856305 in 1608ms cpu (1608ms real) (532527 rewrites/second)
result Summary: States>> 2 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(1, 4) .
rewrites: 298322 in 640ms cpu (640ms real) (466128 rewrites/second)
result Summary: States>> 0 Solutions>> 0
==========================================


 )***

 eq ATTACK-STATE(2) ---  Hijacking
   = :: r :: ---Alice --- Verifier
     [ nil,  -(commit(n(b,r1),s(b,r2))
               @ b : t1 -> a : t2 # i : t3),
              ((t2 === t1 +=+ d(a,b)) and d(a,b) > 0/1),

             +(n(a,r)
               @ a : t2 -> b : t4 # i : t5),

             -(n(a,r) * n(b,r1)
               @ b : t4 -> a : t6 # i : t7),
             ((t6 === t4 +=+ d(a,b)) and d(a,b) > 0/1),
             ((t6 -=- t2) <= (2/1 *=* d) and d > 0/1), --- roundtrip check

             -(s(b,r2)
               @ b : t4 -> a : t9 # i : t10),
             ((t9 === t4 +=+ d(a,b)) and d(a,b) > 0/1),
             (open(n(b,r1),s(b,r2),commit(n(b,r1),s(b,r2))) eq yes),

             -(sign(i,(n(a,r) * n(b,r1)) ; n(a,r))
               @ i : t11 -> a : t12),
             ((t12 === t11 +=+ d(i,a)) and d(i,a) > 0/1) | nil ]
     &
     :: r1,r2 :: ---Bob  --- Prover
     [ nil, +(commit(n(b,r1),s(b,r2))
               @ b : t1 -> a : t2 # i : t3),

             -(n(a,r)
               @ a : t2 -> b : t4 # i : t5),
             ((t4 === t2 +=+ d(a,b)) and d(a,b) > 0/1),

             +(n(a,r) * n(b,r1)
               @ b : t4 -> a : t6 # i : t7), 

             +(s(b,r2)
               @ b : t4 -> a : t9 # i : t10) 

            ---! +(sign(b,(n(a,r) * n(b,r1)) ; n(a,r))
            ---!   @ b : t11' -> a : t12' # i : t13') 
     | nil ]
               
     || empty
     || nil
     || nil
     || nil
  [nonexec] .
  ***(

reduce in MAUDE-NPA : summary(2, 0) .
rewrites: 396 in 4ms cpu (2ms real) (99000 rewrites/second)
result Summary: States>> 1 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(2, 1) .
rewrites: 1123754 in 1236ms cpu (1234ms real) (909186 rewrites/second)
result Summary: States>> 3 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(2, 2) .
rewrites: 2591484 in 3336ms cpu (3337ms real) (776823 rewrites/second)
result Summary: States>> 4 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(2, 3) .
rewrites: 2660917 in 3464ms cpu (3464ms real) (768163 rewrites/second)
result Summary: States>> 3 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(2, 4) .
rewrites: 1575344 in 2356ms cpu (2354ms real) (668651 rewrites/second)
result Summary: States>> 1 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(2, 5) .
rewrites: 388258 in 532ms cpu (533ms real) (729808 rewrites/second)
result Summary: States>> 1 Solutions>> 0
==========================================
reduce in MAUDE-NPA : summary(2, 6) .
rewrites: 288451 in 468ms cpu (466ms real) (616348 rewrites/second)
result Summary: States>> 1 Solutions>> 1
==========================================
reduce in MAUDE-NPA : run(2, 6) .
rewrites: 370 in 4ms cpu (1ms real) (92500 rewrites/second)
result ShortIdSystem: < 1 . 2 . 7 . 6{1} . 3{1} . 1 . 1 > (
:: nil ::
[ nil | 
   -((n(a, #0:Fresh) * n(b, #1:Fresh)) ; n(a, #0:Fresh)
      @ i : #2:Real -> #3:NameTimeSet # i : #4:Real), (#4:Real === #2:Real +=+ 0/1 and 0/1 >= 0/1), 
   +(sign(i, (n(a, #0:Fresh) * n(b, #1:Fresh)) ; n(a, #0:Fresh))
      @ i : #4:Real -> a : #5:Real), nil]  & 
:: nil ::
[ nil | 
   -(n(a, #0:Fresh) * n(b, #1:Fresh)
      @ b : #6:Real -> a : #7:Real # i : #8:Real), (#8:Real === #6:Real +=+ d(b, i) and d(b, i) >=
    0/1), 
   -(n(a, #0:Fresh)
      @ a : #9:Real -> b : #6:Real # i : #10:Real), (#10:Real === #9:Real +=+ d(a, i) and d(a, i) >=
    0/1), (#2:Real >= #8:Real and #2:Real >= #10:Real), 
   +((n(a, #0:Fresh) * n(b, #1:Fresh)) ; n(a, #0:Fresh)
      @ i : #2:Real -> #3:NameTimeSet # i : #4:Real), nil]  & 
:: #0:Fresh ::
[ nil | 
   -(commit(n(b, #1:Fresh), s(b, #11:Fresh))
      @ b : #12:Real -> a : #9:Real # i : #13:Real), (#9:Real === #12:Real +=+ d(a, b) and d(a, b) >
    0/1), 
   +(n(a, #0:Fresh)
      @ a : #9:Real -> b : #6:Real # i : #10:Real), 
   -(n(a, #0:Fresh) * n(b, #1:Fresh)
      @ b : #6:Real -> a : #7:Real # i : #8:Real), (#7:Real === #6:Real +=+ d(a, b) and d(a, b) >
    0/1), ((#7:Real -=- #9:Real) <= (2/1 *=* #14:Real) and #14:Real > 0/1), 
   -(s(b, #11:Fresh)
      @ b : #6:Real -> a : #15:Real # i : #16:Real), (#15:Real === #6:Real +=+ d(a, b) and d(a, b) >
    0/1), 
   yes eq yes, 
   -(sign(i, (n(a, #0:Fresh) * n(b, #1:Fresh)) ; n(a, #0:Fresh))
      @ i : #4:Real -> a : #5:Real), (#5:Real === #4:Real +=+ d(a, i) and d(a, i) > 0/1), nil]  & 
:: #1:Fresh,#11:Fresh ::
[ nil | 
   +(commit(n(b, #1:Fresh), s(b, #11:Fresh))
      @ b : #12:Real -> a : #9:Real # i : #13:Real), 
   -(n(a, #0:Fresh)
      @ a : #9:Real -> b : #6:Real # i : #10:Real), (#6:Real === #9:Real +=+ d(a, b) and d(a, b) >
    0/1), 
   +(n(a, #0:Fresh) * n(b, #1:Fresh)
      @ b : #6:Real -> a : #7:Real # i : #8:Real), 
   +(s(b, #11:Fresh)
      @ b : #6:Real -> a : #15:Real # i : #16:Real), nil] )
| 
(n(a, #0:Fresh)
 @ a : #9:Real -> b : #6:Real # i : #10:Real) !inI,
(s(b, #11:Fresh)
 @ b : #6:Real -> a : #15:Real # i : #16:Real) !inI,
(sign(i, (n(a, #0:Fresh) * n(b, #1:Fresh)) ; n(a, #0:Fresh))
 @ i : #4:Real -> a : #5:Real) !inI,
((n(a, #0:Fresh) * n(b, #1:Fresh)) ; n(a, #0:Fresh)
 @ i : #2:Real -> #3:NameTimeSet # i : #4:Real) !inI,
(commit(n(b, #1:Fresh), s(b, #11:Fresh))
 @ b : #12:Real -> a : #9:Real # i : #13:Real) !inI,
(n(a, #0:Fresh) * n(b, #1:Fresh)
 @ b : #6:Real -> a : #7:Real # i : #8:Real) !inI,
smt(#9:Real === #12:Real +=+ d(a, b) and d(a, b) > 0/1 and (#6:Real === #9:Real +=+ d(a, b) and d(a,
    b) > 0/1 and (#8:Real === #6:Real +=+ d(b, i) and d(b, i) >= 0/1 and (#10:Real === #9:Real +=+ d(
    a, i) and d(a, i) >= 0/1 and (#2:Real >= #8:Real and #2:Real >= #10:Real and (#4:Real === #2:Real
    +=+ 0/1 and 0/1 >= 0/1 and (#7:Real === #6:Real +=+ d(a, b) and d(a, b) > 0/1 and ((#7:Real -=-
    #9:Real) <= (2/1 *=* #14:Real) and #14:Real > 0/1 and (#15:Real === #6:Real +=+ d(a, b) and d(a,
    b) > 0/1 and (#5:Real === #4:Real +=+ d(a, i) and d(a, i) > 0/1))))))))))
| 
+(commit(n(b, #1:Fresh), s(b, #11:Fresh))
   @ b : #12:Real -> a : #9:Real # i : #13:Real), 
-(commit(n(b, #1:Fresh), s(b, #11:Fresh))
   @ b : #12:Real -> a : #9:Real # i : #13:Real), 
+(n(a, #0:Fresh)
   @ a : #9:Real -> b : #6:Real # i : #10:Real), 
-(n(a, #0:Fresh)
   @ a : #9:Real -> b : #6:Real # i : #10:Real), 
+(n(a, #0:Fresh) * n(b, #1:Fresh)
   @ b : #6:Real -> a : #7:Real # i : #8:Real), 
-(n(a, #0:Fresh) * n(b, #1:Fresh)
   @ b : #6:Real -> a : #7:Real # i : #8:Real), 
-(n(a, #0:Fresh)
   @ a : #9:Real -> b : #6:Real # i : #10:Real), 
+((n(a, #0:Fresh) * n(b, #1:Fresh)) ; n(a, #0:Fresh)
   @ i : #2:Real -> #3:NameTimeSet # i : #4:Real), 
-((n(a, #0:Fresh) * n(b, #1:Fresh)) ; n(a, #0:Fresh)
   @ i : #2:Real -> #3:NameTimeSet # i : #4:Real), 
+(sign(i, (n(a, #0:Fresh) * n(b, #1:Fresh)) ; n(a, #0:Fresh))
   @ i : #4:Real -> a : #5:Real), 
+(s(b, #11:Fresh)
   @ b : #6:Real -> a : #15:Real # i : #16:Real), 
-(n(a, #0:Fresh) * n(b, #1:Fresh)
   @ b : #6:Real -> a : #7:Real # i : #8:Real), 
-(s(b, #11:Fresh)
   @ b : #6:Real -> a : #15:Real # i : #16:Real), 
-(sign(i, (n(a, #0:Fresh) * n(b, #1:Fresh)) ; n(a, #0:Fresh))
   @ i : #4:Real -> a : #5:Real)
| 
nil
  )***


endfm

--- THIS HAS TO BE THE LAST LOADED MODULE !!!!
select MAUDE-NPA .

red displayGrammars .

red summary(1,0) . 
red summary(1,1) .
red summary(1,2) .
red summary(1,3) .
red summary(1,4) .

red summary(2,0) . 
red summary(2,1) . 
red summary(2,2) . 
red summary(2,3) . 
red summary(2,4) . 
red summary(2,5) . 
red summary(2,6) . 
red run(2,6) .