The format for the text file is the following (see parsers/tobsLexer.lex and parsers/tobsParser.yacc for more details) :
#trans TNAME #inhib PNAME "ARCVAL" PNAME2 "ARCVAL2" #pre PNAME "ARCVAL" #guard "GUARD" #endtrans #trans TNAME2 ... etc #endtrans
All fields (inhib, pre, guard) are optional. The transition name is mandatory and should be unique. The order inhib/pre/guard is enforced.
PNAME must be a valid place name in your model, and ARCVAL a CAMI arc function expression (in correct extended CAMI syntax) with respect to the domain of PNAME.
An arbitrary number of arcs may be added (to pre or inhib) but no two arcs should reference the same place. At least one and as many transitions as desired can be put in a single file.
Arc functions and guards should be enclosed in double quotes " ".
All names should be legal C identifiers: (_|alpha)(_|alpha|numeric)*
whitespace are ignored, including newlines, however keywords (#trans, #inhibitor, ...) should be placed after a newline.
#trans P1ThinksNotEat #inhibitor Eating "<x>" #pre Thinking "<x>" #guard "[x = 1]" #endtrans
Will be true in any state such that :
there is at least a philosopher x in place Thinking,
that same x is not Eating as well,
this philosopher x is the philosopher 1. (Class Philo is 1..N_PHILO;)
Please note that the syntax accepted is extended CAMI syntax for Well-Formed Nets, it allows reference to static subclasses if they exist. Thus variables have to be declared in the original model.
The atomic properties will have an impact on the state space generated, by changing the static/dynamic subclass declarations of the model generated for GreatSPN.