WARN (Program.cpp:179): The input model is a CTMC, but uses probabilistic commands like they are used in PRISM. Consider rewriting the commands to use Markovian commands instead.
WARN (Program.cpp:1355): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
formula: P=? [true U<=15 (bLoad < 3)]
formula: P=? [F (bPower = 11)]
formula: P=? [F (gState1 = 13)]
WARN (Program.cpp:1355): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
WARN (Program.cpp:1355): The model uses synchronizing Markovian commands. This may lead to unexpected verification results, because of unclear semantics.
checking formula: P=? [true U<=15 (bLoad < 3)]
0.01740805569,0.009222638946,0.9923681004,0.01083402873,0.9972075707,0.01247075564,0.9991433588,0.00486376728,0.9301463393,0.9997886215,0.00620181091,0.9625535065,0.9999606916,0.007673066949,0.9819978069,0.9999951056,0.00193472382,0.7323889666,0.9999996941,0.002741047755,0.815248201,1,0.003752847361,0.8815355885,1,0.000660505001,0.4319104244,1,0.001059344376,0.5343462911,1,0.001641891518,0.6367821577,1,0.000660505001,0.1805282884,1,0.2511412479,1,0.3358767994,1,1,1,1,1,first initial state: 0.01740805569
checking formula: P=? [F (bPower = 11)]
1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,first initial state: 1
checking formula: P=? [F (gState1 = 13)]
1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,1,first initial state: 1