ISModeler combines data and process models. It takes a process model in the form of a CPN model, a Data model in the form of a TPTP specification, and a specification that defines how the transitions in the Petri net manipulate the data population. ISModeler is written in Java, and uses Access/CPN to retrieve the enabled transitions and their binding from the CPN-model. Next, ISModeler checks for each enabled transition whether it is valid according to the E prover.
For this, the constraints need to be specified in the TPTP syntax. ISModeler applies an internal automated prover to check validity for every transition and binding individually. Internally, ISModeler maintains a current population, with an axiom for each of the facts in that population. Validating a transition involves updating the axioms of the population, and running the E-prover for the new population. If a transition is found to be valid, it is added to the list of valid and enabled transitions within the current state.
After checking all enabled transitions for validity, a valid transition is chosen to be executed, either manually, or randomly chosen.
Links:
Screenshot
The picture below shows a screenshot of the tool. On the right you see the population generated by the process in the upper left side. The tool decides which transitions are both enabled and valid, and presents a list to the user to either select a specific transition, or to randomly choose a transition.
