Opened 10 years ago

Last modified 10 years ago

#49 new defect

uCTMDPi: 0-vector for timebound 0

Reported by: Viet Yen Nguyen Owned by:
Priority: major Milestone: MRMC future
Component: Numerical Engine Version: 1.3.1
Keywords: Cc:

Description

Daniel discovered a bug in the uCTMDPi implementation, where the state vector is zero for a timebound 0. See output below:

STATES 6
#DECLARATION
@
reply.request.@
reply
reply.@
request
request.@
#END
1 @

  • 1 0.80
  • 2 0.20

1 @

  • 1 0.900
  • 2 0.100

2 request.@

  • 3 0.100
  • 4 0.100
  • 5 0.80

2 request.@

  • 3 0.1500
  • 4 0.0500
  • 5 0.80

3 @

  • 3 0.100
  • 4 0.100
  • 5 0.80

3 @

  • 3 0.1500
  • 4 0.0500
  • 5 0.80

4 @

  • 4 0.200
  • 6 0.80

5 reply.@

  • 1 0.80
  • 2 0.20

5 reply.@

  • 1 0.900
  • 2 0.100

6 reply.request.@

  • 3 0.100
  • 4 0.100
  • 5 0.80

6 reply.request.@

  • 3 0.1500
  • 4 0.0500
  • 5 0.80

P{<1}[tt U[0,0.0] goal]
P{<1}[tt U[0,10.0] goal]
P{<1}[tt U[0,20.0] goal]
P{<1}[tt U[0,30.0] goal]
P{<1}[tt U[0,40.0] goal]
P{<1}[tt U[0,50.0] goal]
P{<1}[tt U[0,60.0] goal]
P{<1}[tt U[0,70.0] goal]
P{<1}[tt U[0,80.0] goal]
P{<1}[tt U[0,90.0] goal]
P{<1}[tt U[0,100.0] goal]
quit
#DECLARATION
init
goal
#END

1 init
6 goal
4 goal


| Markov Reward Model Checker |
| MRMC version 1.3 |
| Copyright (C) The University of Twente, 2004-2007. |
| Copyright (C) RWTH-Aachen, 2006-2008. |
| Authors: |
| Ivan S. Zapreev (since 2004), Christina Jansen (since 2007), |
| David N. Jansen (since 2007), E. Moritz Hahn (since 2007), |
| Sven Johr (2006-2007), Tim Kemna (2005-2006), |
| Maneesh Khattri (2004-2005) |
| MRMC is distributed under the GPL conditions |
| (GPL stands for GNU General Public License) |
| The product comes with ABSOLUTELY NO WARRANTY. |
| This is a free software, and you are welcome to redistribute it. |


Logic = CSL
Loading the 'closed_Server_![reply,_request]!_![]^2_abstr(Client0_U_Client1_U_Client2_U_Client3_U_Client4,_{rec=[1,_3,_8,_11,_13],_req=[0,_5,_6,_9,_14],_rd=[2,_4,_7,_10,_12]}).ctmdpi' file, please wait.
Loading the 'closed_Server_![reply,_request]!_![]^2_abstr(Client0_U_Client1_U_Client2_U_Client3_U_Client4,_{rec=[1,_3,_8,_11,_13],_req=[0,_5,_6,_9,_14],_rd=[2,_4,_7,_10,_12]}).lab' file, please wait.
The Occupied Space is 776 Bytes.
Type 'help' to get help.
ERROR: Fox-Glynn: lambda = 0, terminating the algorithm
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.0000000, 0.0000000, 0.0000000, 0.0000000, 0.0000000, 0.0000000 )
$STATE: { 1, 2, 3, 4, 5, 6 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
Fox-Glynn: ltp = 0, rtp = 153, w = 9.391435518908349e+296
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.1543761, 0.2325637, 0.2325637, 1.0000000, 0.1543761, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
Fox-Glynn: ltp = 0, rtp = 163, w = 1.241487345595022e+297
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.2971468, 0.3621351, 0.3621351, 1.0000000, 0.2971468, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
ERROR: Fox-Glynn: lambda >= 25, underflow. The results are UNRELIABLE.
Fox-Glynn: ltp = 0, rtp = 173, w = 1.430626769619844e+297
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.4158131, 0.4698291, 0.4698291, 1.0000000, 0.4158131, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
ERROR: Fox-Glynn: lambda >= 25, underflow. The results are UNRELIABLE.
Fox-Glynn: ltp = 6, rtp = 183, w = 1.613492625231256e+297
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.5144444, 0.5593406, 0.5593406, 1.0000000, 0.5144444, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
ERROR: Fox-Glynn: lambda >= 25, underflow. The results are UNRELIABLE.
Fox-Glynn: ltp = 12, rtp = 193, w = 1.763338686962057e+297
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.5964232, 0.6337394, 0.6337394, 1.0000000, 0.5964232, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
ERROR: Fox-Glynn: lambda >= 25, underflow. The results are UNRELIABLE.
Fox-Glynn: ltp = 19, rtp = 203, w = 1.899618880330600e+297
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.6645612, 0.6955770, 0.6955770, 1.0000000, 0.6645612, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
ERROR: Fox-Glynn: lambda >= 25, underflow. The results are UNRELIABLE.
Fox-Glynn: ltp = 25, rtp = 213, w = 2.007768695115810e+297
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.7211950, 0.7469743, 0.7469743, 1.0000000, 0.7211950, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
ERROR: Fox-Glynn: lambda >= 25, underflow. The results are UNRELIABLE.
Fox-Glynn: ltp = 33, rtp = 223, w = 2.123485373742082e+297
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.7682671, 0.7896939, 0.7896939, 1.0000000, 0.7682671, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
ERROR: Fox-Glynn: lambda >= 25, underflow. The results are UNRELIABLE.
Fox-Glynn: ltp = 40, rtp = 233, w = 2.217029960763284e+297
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.8073918, 0.8252010, 0.8252010, 1.0000000, 0.8073918, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).
ERROR: Fox-Glynn: lambda >= 25, underflow. The results are UNRELIABLE.
Fox-Glynn: ltp = 47, rtp = 243, w = 2.300971995732339e+297
$ERROR_BOUND: 1.000000e-06
$MAX_RESULT: ( 0.8399108, 0.8547132, 0.8547132, 1.0000000, 0.8399108, 1.0000000 )
$STATE: { 1, 2, 3, 5 }

The Total Elapsed Model-Checking Time is 0 milli sec(s).

Change History (1)

comment:1 Changed 10 years ago by Dr. Ivan S. Zapreev

The fact that for that property we have

ERROR: Fox-Glynn: lambda = 0, terminating the algorithm

Indicates that Fox-Glynn does not work and probably returns some zero values.
In this case in uCTMDOP model checking, I guess, one has to use the vector of initial probabilities as the result but not follow the original model checking procedure. I do not know the details, but a similar bug was with CTMC model chekcing, where for zero time we had to use the vector of initial probabilities.

PS: By the way, why do not I get any notifications about new tickets any more? Am I off the developers list? I OBJECT!

Note: See TracTickets for help on using tickets.