Sometimes, it may be easier to define the MoCC using automata. For example, we can see a place as something on which we can read a token (ont output transition reads one token) or we can write a token (one input transition writes one token). A token can only be read if there is at least one in the place. Initially, there is as much token in the place as in the initial token count of the place.
For explanations on how to use the MoCCML editor, please refer to the GEMOC manual.
We first define the declaration of a relation (placeReadWrite). Here after is its graphical representation. This relation is parameterized by the r clock (some one how wants to read a token), the w clock (someone how wants to write a token, and n the initial count of token in the place).
Then we can define this relation. Here after is the resulting automaton. The local variable count represent the number of tokens in this place. s0 is the initial state. The action on the transition from s0 to s initialize count with n (the parameter). The two reflexive transitions on s explain what happens when w or r occurs. The write transition is fired when w occurs and a token is assed in the place (count is incremented). The read transition is fired when r occurs. It removes a token and thus decrements count. A guard prevents the read transition to be fired if there is not at liste one token in the place (count >= one).
Here is the textual representation of this constraint automata.
Textual representation of the constraint automata.
AutomataConstraintLibrary markedgraph{
import "platform:/plugin/fr.inria.aoste.timesquare.ccslkernel.model/ccsllibrary/kernel.ccslLib" as kernel;
import "platform:/plugin/fr.inria.aoste.timesquare.ccslkernel.model/ccsllibrary/CCSL.ccslLib" as ccsl;
RelationLibrary placeLib {
AutomataRelationDefinition placeReadWriteDef[placeReadWrite]{
variables {
Integer MAX = 10
Integer count = 0
}
init: s0
from s0 to s : init
-> (do count = n.value)
from s to s : read
-> ( when r if( count >= one) do count = (count - one))
from s to s : write
-> ( when w do count = (count + one))
State s0 (out : init)
State s( in : read, write, init
out : write, read
)
}
RelationDeclaration placeReadWrite(r:clock, w: clock, n: int)
}
}