Simulation of Petri Nets

ECArules are a powerful tool to express semantics of concepts that are not expressible by deductive rules. For example, the semantics of petri nets, in particular the firing of an enabled transition, can be expressed by a single ECArule.

ECArule UpdateConnectedPlaces with
  mode m: Deferred
  rejectMsg rm: "The last firing of a transition failed. 
                 Check whether the transition was enabled!"
  ecarule
        er : $  fire/FireTransition tr/Transition pl/Place 
                n,n1,delta/Integer
        ON Tell( (fire transition tr) )
        IF (tr in EnabledTransition) and
           (pl in ConnectedPlace[tr/trans]) and
           (delta in NetEffectOfTransition[pl/xp,tr/xt]) and
           (pl tokenFill n) and
           (n1 in IPLUS[n/i1,delta/i2])
        DO Untell( (pl tokenFill n) ),
           Tell( (pl tokenFill n1) )
        ELSE
           reject
        $
end

The example shows that the condition can also be a complex logical expression. Note that the event (ON-part) binds the two variables fire and tr. The condition (IF-part) additionally binds the free variables pl, delta, n, and n1. Each binding of the free variables is passed to the DO-part leading to some update of the tokenFill attribute. In case that the IF-part cannot be evaluated to true, the ELSE-part is executed. That will lead to an abortion of the current transaction rolling back all updates and issuing the error message listed under rejectMsg. The complete example of modeling petri nets is in the CB-Forum.

It should be noted that one can also ask queries in the DO-part (and ELSE-part) of an ECArule. Other than for the IF-part, such queries are only evaluated once.