ALGEBRA TruthCCSAC

sorts
  definition, exp, act, restriction, renSet, renaming

cons
  ProcDef	: string * exp -> definition		("_ = _")
  ResDef	: string * restriction -> definition	("_ = _")
  RenDef	: string * renSet -> definition		("_ = _")

  Gate	: exp * exp -> exp			("_ # _")	(CO)
  Par	: exp * exp -> exp			("_ | _")	(AC, CO)
  Plus	: exp * exp -> exp			("_ + _")	(AC)
  Rest	: exp * restriction -> exp		("(_)\\_")
  Ren	: exp * renSet -> exp			("(_)[_]")
  Pref	: act * exp -> exp			("_._")
  Nil	: unit -> exp				("0")
  Var	: string -> exp				("_")

  ResList	: (act list) -> restriction	("{_}")
  ResVar	: string -> restriction		("_")

  RenList	: (renaming list) -> renSet	("_")
  RenVar	: string -> renSet		("_")

  RenPair	: string * string -> renaming	("_/_")

  Action	: bool * string -> act		("_-'--_")
  Tau		: unit -> act			("tau")


pragmas
  { ignore junk }
  { parse all }
  { truth true }

SYNTAX

tokens
  ""	=> TRUE
  ""	=> FALSE
  ""	=> RENAME
  "\\"	=> REST
  "/"	=> SLASH
  "."	=> DOT
  ","	=> KOMMA
  "\("	=> OPENB
  "\)"	=> CLOSEB
  "{"	=> OPENCB
  "}"	=> CLOSECB
  "\["	=> OPENSB
  "\]"	=> CLOSESB
  "#"	=> GATE
  "\+"	=> PLUS
  "\|"	=> PAR
  "'"	=> PRIME
  "tau"	=> TAU
  "0"	=> NIL
  "="	=> EQUAL
  "[A-Z][A-Za-z0-9_']*" => VAR of String
  "[a-z][A-Za-z0-9_']*" => LABEL of String

priorities
  left		10 GATE
  left		20 PAR
  left		30 PLUS
  left		50 RENAME
  left		60 REST
  right		90 DOT

nonterminals
  def of definition		(SYSTEM)
  exp of exp
  pSys of exp			(STATE)
  rest of restriction
  act of act			(ACTION)
  actList of (act list)
  renSet of renSet
  renaming of renaming
  renList of (renaming list)

grammar
  def	: VAR EQUAL pSys	(ProcDef(VAR, pSys))
	| VAR EQUAL OPENCB actList CLOSECB
				(ResDef(VAR, ResList(actList)))
	| VAR EQUAL OPENSB renList CLOSESB
				(RenDef(VAR, RenList(renList)))

  pSys	: OPENB pSys CLOSEB REST rest
				(Rest(pSys, rest))
	| pSys GATE pSys	(Gate(pSys1, pSys2))
	| exp			(exp)

  exp	: NIL	 		(Nil())
	| VAR			(Var(VAR))
	| exp PAR exp		(Par(exp1, exp2))
	| exp PLUS exp		(Plus(exp1, exp2))
	| act DOT exp		(Pref(act, exp))
	| exp REST rest		(Rest(exp, rest))
	| exp RENAME renSet 	(Ren(exp, renSet))
	| OPENB exp CLOSEB	(exp)


  rest	: VAR			(ResVar(VAR))
	| OPENCB actList CLOSECB
				(ResList(actList))

  actList : act + (KOMMA)

  act	: TAU			(Tau())
	| LABEL FALSE		(Action(FALSE, LABEL))
	| PRIME LABEL TRUE	(Action(TRUE, LABEL))

  renSet	: OPENSB VAR CLOSESB
				(RenVar(VAR))
		| OPENSB renList CLOSESB
				(RenList(renList))

  renList	: renaming + (KOMMA)

  renaming	: LABEL SLASH LABEL	(RenPair(LABEL1, LABEL2))


SEMANTIC

vars
  a, b : act
  X, Y, X', Y' : exp
  res : restriction
  Acts : (act list)
  rSet : renSet
  renames : (renaming list)
  P, R, l, m : string
  bool : bool

equations

(Nil4Plus)
	X + 0 -> X
(Sym4Plus)
	X + X -> X
(Nil4Par)
	X | 0 -> X
(Nil4Rest)
	0\res -> 0
(FlatRest)
	X\res\res -> X\res
(Nil4Ren)
	0rSet -> 0
(FlatRen)
	X rSet rSet -> X rSet

rules

-- The rules for the standard CCS cases.

	 P = X in Set, X -(a)-> Y
(Insert)--------------------------
		Var(P) -(a)-> Y



(Action)-----------------------
		a.X -(a)-> X


	 ("bool isNotPlus X tau"), X -(a)-> X'
(Choice)--------------------------------------
		X + Y -(a)-> X'


-- Not needed, as | was made compatible.
--	     X -(a)-> X'
--(Par)-------------------------
--	X | Y -(a)-> X' | Y


	 X -(a)-> X', Y -(b)-> Y', ("bool isInverseAction a b")
(GateSync)--------------------------------------------------------
		 X # Y -(tau)-> X' # Y'


	 ("bool isNotPar X tau"), X -(a)-> X', Y -(b)-> Y', ("bool isInverseAction a b")
(Sync)----------------------------------------------------------------------------------
		 		X | Y -(tau)-> X' | Y'


	X -(a)-> X', ("bool isNotElemInActList a Acts")
(Rest)--------------------------------------------------
		X\{Acts} -(a)-> X'\{Acts}


	R = {Acts} in Set, X -(a)-> X', ("bool isNotElemInActList a Acts")
(RestVar)-------------------------------------------------------------------
				X\R -(a)-> X'\R


		X -(Action(bool, l))-> X', ("list RenPair(m, l) renames")
(Renaming)----------------------------------------------------------------
		X[renames] -(Action(bool, m))-> X'[renames]


		X -(a)-> X', ("bool isNotRenamed a renames")
(ThroughRen)---------------------------------------------------
			X[renames] -(a)-> X'[renames]


	R = [renames] in Set, X -(Action(bool, l))-> X', ("list RenPair(m, l) renames")
(RenamingVar)--------------------------------------------------------------------------
			X[R] -(Action(bool, m))-> X'[R]


	R = [renames] in Set, X -(a)-> X', ("bool isNotRenamed a renames")
(ThroughRenVar)-----------------------------------------------------------
				X[R] -(a)-> X'[R]

end