Consistency Checker
The consistency checker can check consistency between choreography milestone models, choreography scenario models and provider behaviour models. It implements the theory presented in this technical report. The (Petri net) models can be constructed using the Petri Net Kernel. They can also be constructed by transforming BPMN models to Petri nets, using the BPMN transformer.
The tool can be started from the command prompt. Starting it without arguments, will show the acceptable arguments. The example from the technical report is included in the .zip file. To check consistency between the included milestone model and scenario models, type:
java -jar CheckConsistency.jar -MS Milestone.pnml Scenario1.pnml Scenario2.pnml
To check consistency between the included provider behaviour model and scenario models, type:
java -jar CheckConsistency.jar -PS Provider.pnml Scenario1.pnml Scenario2.pnml