GSPN->JANI->Model checking: Labelling inconsistent.

[sjunges]

When working on stormpy, @volkm hinted at the following discrepancy that likely is a bug. This is work in progress :-)

~/i2/storm/release-build/bin/storm --jani ~/Documents/petrinet.jani --prop "Pmax=? [F deadl]" --buildfull Storm 1.6.1 (dev) Time for model input parsing: 0.002s.

Time for model construction: 0.044s.

---

Model type: CTMC (sparse) States: 34 Transitions: 89 Reward Models: none State Labels: 3 labels

• deadlock -> 1 item(s)
• init -> 1 item(s)
• deadl -> 1 item(s) Choice Labels: none

---

Model checking property "1": Pmax=? [F deadl] ... Result (for initial states): 1

VS

~/i2/storm/release-build/bin/storm --jani ~/Documents/petrinet.jani --prop "Pmax=? [F deadl]" Storm 1.6.1 (dev) Time for model input parsing: 0.008s.

Time for model construction: 0.033s.

---

Model type: CTMC (sparse) States: 34 Transitions: 89 Reward Models: none State Labels: 3 labels

• deadlock -> 1 item(s)
• init -> 1 item(s)
• deadl -> 0 item(s) Choice Labels: none

---

Model checking property "1": Pmax=? [F deadl] ... Result (for initial states): 0 Time for model checking: 0.001s.

petrinet.jani.zip