Browse Source

Sim bug: temporal operator types.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@717 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 18 years ago
parent
commit
574f6e9ebb
  1. 6
      prism/src/simulator/SimulatorEngine.java

6
prism/src/simulator/SimulatorEngine.java

@ -2179,16 +2179,16 @@ public class SimulatorEngine
switch (exprTemp.getOperator()) {
case ExpressionTemporal.P_X:
if (exprTemp.getOperand2().getType() != Expression.PATH_BOOLEAN)
if (exprTemp.getOperand2().getType() != Expression.BOOLEAN)
return -1;
exprPtr2 = exprTemp.getOperand2().toSimulator(this);
return loadPctlNext(exprPtr2);
case ExpressionTemporal.P_U:
if (exprTemp.getOperand1().getType() != Expression.PATH_BOOLEAN)
if (exprTemp.getOperand1().getType() != Expression.BOOLEAN)
return -1;
exprPtr1 = exprTemp.getOperand1().toSimulator(this);
if (exprTemp.getOperand2().getType() != Expression.PATH_BOOLEAN)
if (exprTemp.getOperand2().getType() != Expression.BOOLEAN)
return -1;
exprPtr2 = exprTemp.getOperand2().toSimulator(this);
if (exprTemp.hasBounds()) {

Loading…
Cancel
Save