search

utwente-fmt / DFTRES

Rare event simulation tool for Dynamic Fault Trees
GNU General Public License v3.0
4 stars 3 forks source link

Nondeterminism reported for DTMC JANI model #1

Closed hobborg closed 4 years ago

hobborg commented 4 years ago

The QComp 2020 benchmarks include several DTMC models, among them the coupons.9-4 JANI file.
When running DFTRES on that file with the following command line, "nondeterminism" is reported in a probabilistic transition, even though the JANI file is of type DTMC.

java -jar DFTRES.jar --progress -s 0 --relErr 5e-2 --prop collect_all_bounded --def B 5 coupon.9-4.jani
hobborg commented 4 years ago

The coupons JANI model was generated by Storm from a PGCL file, so I was suspecting the issue could be related to the PGCL → JANI translation.
However, the same issue occurs with DTMCs that were converted from PRISM models, e.g. crowds using the following command:

java -jar DFTRES.jar -s 0 --relErr 5e-2 --prop collect_all_bounded --def TotalRuns 5 --def CrowdSize 10 crowds.jani
ennoruijters commented 4 years ago

Fixed, the nondeterminism detection wasn't properly resetting between states and wrongly detecting both interactive and probabilistic transitions. Crowds now works (coupons parses but the property is unsupported).