Formula generation, how to

1. Build the formula generator mcc using the create-phar.sh script
2. Put all the directories (or .tgz archives) containing the models in a folder models
3. Modify the generate_formulas.sh script, setting the value of the ROOT variable as the path to your models folder
4. Use generate_formulas.sh, which will generate the formulas
5. The file output-1000states.txt contains information on what happened during the generation, check it

Requirements

• Php for the mcc tool
• Python with the argparse and networkx packages for the smc tool used for filtering out formulas

Formula generation, hold reminders

• First, execute the model:fix command to normalize the internal references (ids) of the PNML files contining the P/T model of every colored model. The formula generation process needs to establish the correspondance between colored transitions and the corresponding ones in the unfolded P/T model. Hence the need of this step. Check if everything is ok using the model:check-unfolding command.

• Then, the formula::generate randomly generate the formula for any colored model and for any P/T model which has not been generated by un unfolding of an associated colored model.

• Finally, the formula::unfold searches any P/T model that has been generated by an unfolding process out of a colored model. For each one of them, unfolds the formulae generated (or hand written) for the colored model, producing a set of formulae for the P/T model. Such formulae are equivalent to the original ones, in the sense that the colored formula is satsifiable in the colored model iff the unfolded formula is satisfiable in the unfolded P/T model

  This process will only update the is-firable() propositions, substituting the colored transition for the equivalent unfolded ones, and analogously for the token-count() and place-bound() operators.

TODO

• formal semantics of the property language, in particular with regard to token-count() and color nets, and strict/unstrict bounds for place-bound()