% Source: http://www.cs.kuleuven.ac.be/~dtai/prototypes/dppd/petri-meta.html
tr(Tr,X,St) :-
	trace(Tr,[X,s(0),0,0,0],St).
	
trace([],State,State).
trace([Action|As],InState,OutState) :-
	trans(Action,InState,S1),
	trace(As,S1,OutState).

trans(enter_cs,[s(X),s(Sema),CritSec,Y,C],
	       [X,Sema,s(CritSec),Y,C]).
trans(exit_cs, [X,Sema,s(CritSec),Y,C],
	       [X,s(Sema),CritSec,s(Y),C]).
trans(restart, [X,Sema,CritSec,s(Y),ResetCtr],
	       [s(X),s(Sema),CritSec,Y,s(ResetCtr)]).