HELP: Is it possible to convert a BPMN to a TPN file?

[DigitalGabriele]

I need to do formal model check on my BPMN. I found your great repo and I was able to convert my files to a Petri-net. Now I need to use a formal model checker to verify the newly created Petri-net. Unfortunately, the other model checkers don't seem to accept the file I generated using your library.

I tried TINA and ROMEO and neither accepted the file.

I used the following code:

class Variants(Enum):
    PNML = pnml

PNML = Variants.PNML

bpmn = pm4py.read_bpmn(bpmn_path)
net, initial_marking, final_marking = pm4py.convert_to_petri_net(bpmn)

output_filename = "simple_bpmn_converted_to_petri_net.tpn"
parameters = None
variant = PNML

exec_utils.get_variant(variant).export_net(net, initial_marking, output_filename,
                                                      final_marking=final_marking, parameters=parameters)

In the paper it mentions that LTL checker is part of the Conformance checking. From what I understand reading your paper, pm4py validates against real world data. It doesn't do formal checking, correct?

[fit-alessandro-berti]

Dear @DigitalGabriele , we don't offer support for exporting the TPN format.

LTL Checking is mainly implemented in a couple of filters (Four Eyes Principle and Activity done by different Resources). So the input is an event log and a rule, and the output is an event log containing the cases for which the rule is satisfied