*** ccs-modular.maude

*** modular semantics of CCS.  Two different semantic definitions are
*** given: one the standard semantics, and another a weak trace semantics
*** in which silent (tau) steps are ignored; note that in this modular
*** setting there is no need to change the semantic rules when one semantics
*** is replaced by the other.


fmod RECORD is 
 sorts Index Component Field PreRecord Record .
 subsort Field < PreRecord .

 op null : -> PreRecord [ctor] .
 op _,_ : PreRecord PreRecord -> PreRecord [ctor assoc comm id: null] .
 op _:_ : [Index] [Component] -> [Field] [ctor] .
 op {_} : [PreRecord] -> [Record] [ctor] .
 op duplicated : [PreRecord] -> [Bool] .
 var i : Index . vars c c' : Component . var pr : PreRecord .
 eq duplicated((i : c),(i : c'), pr) = true .
 cmb {pr} : Record if duplicated(pr) =/= true .
endfm

mod RCONF is
 inc RECORD .
 sorts Program Conf .
 op <_,_> : Program Record -> Conf [ctor] .
 op {_,_} : [Program] [Record] -> [Conf] [ctor] .
 op [_,_] : [Program] [Record] -> [Conf] [ctor] .

 vars p p' : Program .  vars r r' : Record .

 crl [step] : < p , r > => < p' , r' > if {p,r} => [p',r'] .
endm

fmod ACTION is
  protecting QID .
  
  sorts Label Act .
  subsorts Qid < Label < Act .
 
  op tau : -> Act .
  op ~_ : Label -> Label [prec 10] .

  eq ~ ~ l:Label = l:Label .
endfm

fmod PROCESS is  
  protecting ACTION .

  sorts ProcessId Process .
  subsorts Qid < ProcessId < Process .

  op 0 : -> Process .                
  op _._ : Act Process -> Process [prec 25] . 
  op _+_ : Process Process -> Process [assoc comm prec 35] .
  op _|_ : Process Process -> Process [assoc comm prec 30] .
  op _[_/_] : Process Label Label -> Process [prec 20] .
  op _\_ : Process Label -> Process [prec 20] . 
endfm


fmod CCS-CONTEXT is
  extending PROCESS .
  sorts Process? Context .
  subsort Process < Process? .

  op _=def_ : ProcessId Process -> Context [prec 40] .
  op nil : -> Context .
  op _&_ : Context Context -> Context [assoc comm id: nil prec 42] .
  op _definedIn_ : ProcessId Context -> Bool .
  op def : ProcessId Context -> Process? .
  op not-defined : -> Process? .

  op context : -> Context .

  var x : ProcessId .
  var p : Process .
  var c : Context .

  eq x definedIn (x =def p & c) = true .
  eq x definedIn c = false [owise] .
  eq def(x,(x =def p & c)) = p .
  eq def(x, c) = not-defined [owise] .
endfm


fmod ACTION-LIST is
  protecting ACTION .
  
  sort ActList .
  subsort Act < ActList .

  op mt : -> ActList .
  op __ : ActList ActList -> ActList [ctor assoc id: mt] .
endfm

mod CCS-SEMANTICS is
  protecting CCS-CONTEXT .
  including RCONF .
  protecting ACTION-LIST .

  sort Trace . 
  subsort Process < Program .
  subsort Trace < Component .

  op tr : -> Index .

  op nil : -> Trace .                        *** abstract interface
  op _;_ : Trace Act -> Trace .              *** abstract interface
  
  op   [_] : ActList -> Trace [ctor] .      *** concrete sort coercion

  vars l m : Label .
  var a : Act .
  vars p p' q q' : Process .
  var x : ProcessId .
  var t : Trace .
  vars al al' : ActList .
  var pr : PreRecord .

  mb tr : t : Field .
  
  eq [al] ; a = [al a] .

  *** Prefix
  rl {a . p,{(tr : t), pr}} => [p,{(tr : t ; a) , pr}] .

  *** Summation
  crl {p + q,{(tr : t), pr}} => [p',{(tr : t ; a), pr}] 
                      if {p,{(tr : nil), pr}} => [p',{(tr : nil ; a), pr}] .

  *** Composition
  crl {p | q,{(tr : t), pr}} => [p' | q,{(tr : t ; a), pr}] 
                      if {p,{(tr : nil), pr}} => [p',{(tr : nil ; a), pr}] .
  crl {p | q,{(tr : t), pr}} => [p' | q',{(tr : t ; tau), pr}] 
                if {p,{(tr : nil), pr}} => [p',{(tr : nil ; l), pr}] /\
                   {q,{(tr : nil), pr}} => [q',{(tr : nil ; (~ l)), pr}] .

  *** Restriction
  crl {p \ l,{(tr : t), pr}} => [(p' \ l),{(tr : t ; a), pr}] if
    {p,{(tr : nil), pr}} => [p',{(tr : nil ; a), pr}] /\ a =/= l /\ a =/= ~ l .
                         
  *** Relabelling
  crl {p[m / l],{(tr : t), pr}} => [(p'[m / l]), {(tr : t ; m), pr}] 
                          if {p,{(tr : nil),pr}} => [p',{(tr : nil ; l),pr}] .
  crl {p[m / l],{(tr : t), pr}} => [(p'[m / l]),{(tr : t ; (~ m)), pr}] 
                      if {p,{(tr : nil),pr}} => [p',{(tr : nil ; (~ l)),pr}] .
  crl {p[m / l],{(tr : t), pr}} => [(p'[m / l]),{(tr : t ; a),pr}] if
    {p,{(tr : nil), pr}} => [p',{(tr : nil ; a), pr}] /\ a =/= l /\ a =/= ~ l .

  *** Definition
  crl {x,{(tr : t), pr}} => [p,{(tr : t ; a), pr}] if (x definedIn context)
         /\ {def(x,context),{(tr : nil),pr}} => [p,{(tr : nil ; a),pr}] .

endm

mod EXAMPLE is
  inc CCS-SEMANTICS .
  
  eq context =  ('Proc =def 'a . 'b . 'Proc) &
                ('Proc2   =def  'a . tau . 'Proc2 + tau . 'b . 'Proc2) & 
                ('Ven    =def  '2p . 'VenB  +  '1p . 'VenL)  & 
                ('VenB   =def  'big . 'collectB . 'Ven)    & 
                ('VenL   =def  'little . 'collectL . 'Ven)   & 
                ('Road   =def  'car . 'up . ~ 'ccross . ~ 'down . 'Road)  & 
                ('Rail   =def  'train . 'green . ~ 'tcross . ~ 'red . 'Rail) & 
                ('Signal =def  ~ 'green . 'red . 'Signal 
                               + ~ 'up . 'down . 'Signal)  & 
                ('Crossing =def (('Road | ('Rail | 'Signal)) 
                                  \ 'green \ 'red \ 'up \ 'down ))  .

endm


search < ('a . 'b . 0 | ~ 'a . 0),{tr : [mt]} > =>1 < p:Process , r:Record > .

search [1] < 'Proc ,{tr : [mt]} > =>+ < p:Process , {tr : ['a 'b 'a]} > .

mod WEAK-CCS-SEMANTICS is
  extending CCS-SEMANTICS .

  op   <_> : ActList -> Trace [ctor] .         *** concrete sort coercion

  vars al al' : ActList .
  var a : Act .

  eq < al tau al' > = < al al' > .
  eq < al > ; a = < al a > .
endm

mod WEAK-EXAMPLE is
  inc WEAK-CCS-SEMANTICS .
  
  eq context =  ('Proc =def 'a . 'b . 'Proc) &
                ('Proc2   =def  'a . tau . 'Proc2 + tau . 'b . 'Proc2) & 
                ('Ven    =def  '2p . 'VenB  +  '1p . 'VenL)  & 
                ('VenB   =def  'big . 'collectB . 'Ven)    & 
                ('VenL   =def  'little . 'collectL . 'Ven)   & 
                ('Road   =def  'car . 'up . ~ 'ccross . ~ 'down . 'Road)  & 
                ('Rail   =def  'train . 'green . ~ 'tcross . ~ 'red . 'Rail) & 
                ('Signal =def  ~ 'green . 'red . 'Signal 
                               + ~ 'up . 'down . 'Signal)  & 
                ('Crossing =def (('Road | ('Rail | 'Signal)) 
                                  \ 'green \ 'red \ 'up \ 'down ))  .

endm

search < ('a . 'b . 0 | ~ 'a . 0),{tr : < mt >} > =>1 < p:Process , r:Record > .

search [1] < 'Proc,{tr : < mt >} > =>+ < p:Process , {tr : < 'a 'b 'a >} > .

search < tau . 'a . tau . 'b . 0,{tr : < mt >} > =>+ < p:Process ,{tr : < 'a >} > .

search [2] < 'Proc2,{tr : < mt >} > =>+ < p:Process,{tr : < 'b 'a >} > .