hlsyounes
commented
9 years ago Confirmed. I see the simulator getting to this state when using the sampling engine:
c=3 & s1=2 & u1=1 & v1=0 & p1=0 & s2=2 & u2=0 & v2=0 & p2=0 & s3=2 & u3=0 & v3=0 & p3=0 & s4=2 & u4=0 & v4=0 & p4=1
The event associated with the "done" action should be enabled in this state, transitioning to state:
c=3 & s1=3 & u1=false & v1=0 & p1=0 & s2=2 & u2=false & v2=0 & p2=0 & s3=2 & u3=false & v3=0 & p3=0 & s4=2 & u4=false & v4=0 & p4=1
However, it doesn't look like the simulator sees this event and thinks the first state is an absorbing state.
The mixed engine also seems to think there are absorbing states, so there is likely something wrong in how the model gets compiled.
When sampling from http://www.prismmodelchecker.org/benchmarks/models/dtmcs/leader_sync/leader_sync4_4.pm, Ymer often prematurly stops extending the path. As a result property P>=0.95 [ F "elected" ] is reported as false on this model. It seems Ymer sees a deadlock state, which does not exist.