The Data & Process Synergizer (DPS) 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. DPS is written in Java, and uses Access/CPN to retrieve the enabled transitions and their binding from the CPN-model. Next, DPS 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. The DPS applies the E Theorem Prover by checking validity for every transition and binding individually.
Internally, DPS 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 by DPS.
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.