ALGEBRA PetriTruth

sorts
	netState, env

cons
	U	: netState * netState -> netState	("_u_")		(AC)
	Token	: string -> netState			("_")
	Empty	: unit -> netState			("0")
	Var	: string -> netState			("_")

	Trans	: string * netState * netState -> env	("_: _ -> _")
	State	: string * netState -> env		("_ = _")

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

SYNTAX

tokens
	"u"		=> U
	":"		=> DOTS
	"="		=> EQUAL
	"\->"		=> ARROW
	"0"		=> EMPTY
	"[a-z]"		=> TOKEN of String
	"[A-Z][A-Za-z0-9'_]*"	=> VAR of String
	"[a-z][A-Za-z0-9'_]+"	=> LABEL of String

priorities
	left	42	U

nonterminals
	env	of env			(SYSTEM)
	state	of netState		(STATE)
	name	of string		(ACTION)

grammar
	env	: name  DOTS state ARROW state	(Trans(name, state1, state2))
		| VAR  EQUAL state		(State(VAR, state))

	state	: state U state		(U(state1, state2))
		| TOKEN			(Token(TOKEN))
		| EMPTY			(Empty())
		| VAR			(Var(VAR))

	name	: LABEL			(LABEL)

SEMANTIC

vars
	State, Rest, Enable, After : netState
	TName, varName : string

equations
(RmEmpty)
	State u 0 -> State

rules


	varName = State in Set, State -(TName)-> After
(LookUp)------------------------------------------------
		Var(varName) -(TName)-> After


	TName: Enable -> After in Set, ("eq State u 0   Enable u Rest")
(Fire)-------------------------------------------------------------
		  State -(TName)-> Rest u After

--	   TName: Enable -> After in Set
--(Step)------------------------------------------
--	Rest u Enable -(TName)-> Rest u After

end