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.

Links:

  • The files of the running example can be found here.
  • The source code of the DPS can be found here.
DPS – Data & Process Synergizer

Leave a Reply

Your email address will not be published. Required fields are marked *