search

moves-rwth / storm

A Modern Probabilistic Model Checker
https://www.stormchecker.org
GNU General Public License v3.0
133 stars 74 forks source link

Jani Dd Model Builder builds incorrect model #57

Closed tquatmann closed 4 years ago

tquatmann commented 4 years ago

For this Jani model I would expect 3 states and a resulting probability of 0.6. The sparse engine and mcsta confirm this. However, the dd engine yields the following:

storm --jani ddbug.jani -jprop -e dd
Storm 1.3.1 (dev)

Date: Tue Oct 15 14:50:27 2019
Command line arguments: --jani ddbug.jani -jprop -e dd
Current working directory: /Users/tim/storm/build/bin

Time for model input parsing: 0.000s.

 WARN (DdJaniModelBuilder.cpp:1521): Guard of an edge in a DTMC overlaps with previous guards.
Time for model construction: 0.012s.

-------------------------------------------------------------- 
Model type:     DTMC (symbolic)
States:     5 (4 nodes)
Transitions:    11 (19 nodes)
Reward Models:  none
Variables:  rows: 2 meta variables (3 DD variables), columns: 2 meta variables (3 DD variables)
Labels:     2
   * deadlock -> 1 state(s) (4 nodes)
   * init -> 1 state(s) (4 nodes)
-------------------------------------------------------------- 

Model checking property "1": Pmin=? [F (X = 1)] ...
Result (for initial states): 0.7999998746
Time for model checking: 0.001s.

The warning is a little suspicious, as there are in fact no overlapping guards. The problem does not occur if we remove the action labels.

cdehnert commented 4 years ago

This should be fixed as of commit 0842cb1b. Can you verify this? Also: I hope that I did not break building other models. The tests are running fine, but if more models are available, it might make sense to validate the changes.

tquatmann commented 4 years ago

I tested a few models, seems to work fine so far. Many thanks!