s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Support (symbolic/explicit) for expected reward to satisfy a co-safe LTL formula. 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10334 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 11 years ago
parent
b037bdf604
commit
957148215e
7 changed files with 558 additions and 204 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 66
      prism/src/explicit/MDPModelChecker.java
  2. 30
      prism/src/explicit/ProbModelChecker.java
  3. 34
      prism/src/explicit/Product.java
  4. 393
      prism/src/parser/PrismParser.java
  5. 18
      prism/src/parser/PrismParser.jj
  6. 3
      prism/src/parser/visitor/TypeCheck.java
  7. 218
      prism/src/prism/NondetModelChecker.java

66
prism/src/explicit/MDPModelChecker.java
View File

@ -49,6 +49,7 @@ import acceptance.AcceptanceType;
import explicit.rewards.MCRewards;
import explicit.rewards.MCRewardsFromMDPRewards;
import explicit.rewards.MDPRewards;
import explicit.rewards.Rewards;
/**
* Explicit-state model checker for Markov decision processes (MDPs).
@ -135,6 +136,71 @@ public class MDPModelChecker extends ProbModelChecker
return probs;
}
/**
* Compute rewards for a co-safe LTL reward operator.
*/
protected StateValues checkRewardCoSafeLTL(Model model, Rewards modelRewards, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException
{
LTLModelChecker mcLtl;
MDPRewards productRewards;
StateValues rewardsProduct, rewards;
MDPModelChecker mcProduct;
LTLModelChecker.LTLProduct<MDP> product;
// For LTL model checking routines
mcLtl = new LTLModelChecker(this);
AcceptanceType[] allowedAcceptance = {
AcceptanceType.RABIN,
AcceptanceType.REACH
};
product = mcLtl.constructProductMDP(this, (MDP)model, expr, statesOfInterest, allowedAcceptance);
// Adapt reward info to product model
productRewards = product.liftFromModel((MDPRewards) modelRewards);
// Output product, if required
if (getExportProductTrans()) {
mainLog.println("\nExporting product transition matrix to file \"" + getExportProductTransFilename() + "\"...");
product.getProductModel().exportToPrismExplicitTra(getExportProductTransFilename());
}
if (getExportProductStates()) {
mainLog.println("\nExporting product state space to file \"" + getExportProductStatesFilename() + "\"...");
PrismFileLog out = new PrismFileLog(getExportProductStatesFilename());
VarList newVarList = (VarList) modulesFile.createVarList().clone();
String daVar = "_da";
while (newVarList.getIndex(daVar) != -1) {
daVar = "_" + daVar;
}
newVarList.addVar(0, new Declaration(daVar, new DeclarationIntUnbounded()), 1, null);
product.getProductModel().exportStates(Prism.EXPORT_PLAIN, newVarList, out);
out.close();
}
// Find accepting states + compute reachability rewards
BitSet acc;
if (product.getAcceptance() instanceof AcceptanceReach) {
// For a DFA, just collect the accept states
mainLog.println("\nSkipping end component detection since DRA is a DFA...");
acc = ((AcceptanceReach)product.getAcceptance()).getGoalStates();
} else {
// Usually, we have to detect end components in the product
mainLog.println("\nFinding accepting end components...");
acc = mcLtl.findAcceptingECStates(product.getProductModel(), product.getAcceptance());
}
mainLog.println("\nComputing reachability rewards...");
mcProduct = new MDPModelChecker(this);
mcProduct.inheritSettings(this);
rewardsProduct = StateValues.createFromDoubleArray(mcProduct.computeReachRewards((MDP)product.getProductModel(), productRewards, acc, false).soln, product.getProductModel());
// Mapping rewards in the original model
rewards = product.projectToOriginalModel(rewardsProduct);
rewardsProduct.clear();
return rewards;
}
// Numerical computation functions
/**

30
prism/src/explicit/ProbModelChecker.java
View File

@ -37,7 +37,10 @@ import parser.ast.ExpressionStrategy;
import parser.ast.ExpressionTemporal;
import parser.ast.ExpressionUnaryOp;
import parser.ast.RewardStruct;
import parser.type.TypeBool;
import parser.type.TypeDouble;
import parser.type.TypePathBool;
import parser.type.TypePathDouble;
import prism.IntegerBound;
import prism.OpRelOpBound;
import prism.PrismComponent;
@ -884,7 +887,7 @@ public class ProbModelChecker extends NonProbModelChecker
{
StateValues rewards = null;
if (expr instanceof ExpressionTemporal) {
if (expr.getType() instanceof TypePathDouble) {
ExpressionTemporal exprTemp = (ExpressionTemporal) expr;
switch (exprTemp.getOperator()) {
case ExpressionTemporal.R_F:
@ -903,6 +906,8 @@ public class ProbModelChecker extends NonProbModelChecker
default:
throw new PrismNotSupportedException("Explicit engine does not yet handle the " + exprTemp.getOperatorSymbol() + " reward operator");
}
} else if (expr.getType() instanceof TypePathBool || expr.getType() instanceof TypeBool) {
rewards = checkRewardPathFormula(model, modelRewards, expr, minMax, statesOfInterest);
}
if (rewards == null)
@ -1044,6 +1049,29 @@ public class ProbModelChecker extends NonProbModelChecker
return StateValues.createFromDoubleArray(res.soln, model);
}
/**
* Compute rewards for a path formula in a reward operator.
*/
protected StateValues checkRewardPathFormula(Model model, Rewards modelRewards, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException
{
if (expr instanceof ExpressionTemporal && ((ExpressionTemporal) expr).getOperator() == ExpressionTemporal.P_F){
return checkRewardReach(model, modelRewards, (ExpressionTemporal) expr, minMax, statesOfInterest);
}
else if (Expression.isCoSafeLTLSyntactic(expr)) {
return checkRewardCoSafeLTL(model, modelRewards, expr, minMax, statesOfInterest);
}
throw new PrismException("Invalid contents for an R operator: " + expr);
}
/**
* Compute rewards for a co-safe LTL reward operator.
*/
protected StateValues checkRewardCoSafeLTL(Model model, Rewards modelRewards, Expression expr, MinMax minMax, BitSet statesOfInterest) throws PrismException
{
// To be overridden by subclasses
throw new PrismException("Computation not implemented yet");
}
/**
* Model check an S operator expression and return the values for all states.
*/

34
prism/src/explicit/Product.java
View File

@ -29,6 +29,9 @@ package explicit;
import java.util.BitSet;
import explicit.rewards.MDPRewards;
import explicit.rewards.MDPRewardsSimple;
import explicit.rewards.StateRewardsConstant;
import parser.type.TypeBool;
import parser.type.TypeDouble;
import parser.type.TypeInt;
@ -142,6 +145,37 @@ public abstract class Product<M extends Model> implements ModelTransformation<M,
return result;
}
/**
* Lifts an MDP reward structure over states in the original model to one
* over states in the product model: The rewards for a product state are
* copied from those the parameter for the corresponding original model state.
* It is assumed that the original model in the product was an MDP.
* It is also assume that nondeterministic choices in each state of the product
* are ordered in the same way as in the original model.
* @param mdpRewards an MDPRewards over states of the original model for this product.
*/
public MDPRewards liftFromModel(MDPRewards mdpRewards)
{
MDP productMDP = (MDP)productModel;
// Special case: constant state rewards
if (mdpRewards instanceof StateRewardsConstant) {
return ((StateRewardsConstant) mdpRewards).deepCopy();
}
// Normal: state and transition rewards
else {
int numStates = productMDP.getNumStates();
MDPRewardsSimple rewSimple = new MDPRewardsSimple(numStates);
for (int productState = 0; productState < numStates; productState++) {
rewSimple.setStateReward(productState, mdpRewards.getStateReward(getModelState(productState)));
int numChoices = productMDP.getNumChoices(productState);
for (int i = 0; i < numChoices; i++) {
rewSimple.setTransitionReward(productState, i, mdpRewards.getTransitionReward(getModelState(productState), i));
}
}
return rewSimple;
}
}
/**
* Project state values from the product model back to the original model. This function
* assumes that the product model has at most one initial state per state in the original

393
prism/src/parser/PrismParser.java
View File

@ -2865,33 +2865,59 @@ public class PrismParser implements PrismParserConstants {
// Contents of an R operator
static final public Expression ExpressionRewardContents(boolean prop, boolean pathprop) throws ParseException {
Expression expr = null;
ExpressionTemporal ret = null;
ExpressionTemporal exprTemp = null;
Expression ret = null;
Token begin;
begin = getToken(1);
if (jj_2_17(2147483647)) {
begin = jj_consume_token(C);
jj_consume_token(LE);
expr = Expression(false, false);
ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); ret.setUpperBound(expr);
exprTemp = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); exprTemp.setUpperBound(expr); ret = exprTemp;
} else {
switch ((jj_ntk==-1)?jj_ntk():jj_ntk) {
case C:
begin = jj_consume_token(C);
ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null);
jj_consume_token(C);
ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null);
break;
case I:
begin = jj_consume_token(I);
jj_consume_token(I);
jj_consume_token(EQ);
expr = Expression(false, false);
ret = new ExpressionTemporal(ExpressionTemporal.R_I, null, null); ret.setUpperBound(expr);
break;
case F:
begin = jj_consume_token(F);
expr = Expression(prop, pathprop);
ret = new ExpressionTemporal(ExpressionTemporal.R_F, null, expr);
exprTemp = new ExpressionTemporal(ExpressionTemporal.R_I, null, null); exprTemp.setUpperBound(expr); ret = exprTemp;
break;
case S:
begin = jj_consume_token(S);
ret = new ExpressionTemporal(ExpressionTemporal.R_S, null, null);
jj_consume_token(S);
ret = new ExpressionTemporal(ExpressionTemporal.R_S, null, null);
break;
case A:
case E:
case FALSE:
case FILTER:
case FUNC:
case F:
case G:
case MAX:
case MIN:
case X:
case PMAX:
case PMIN:
case P:
case RMAX:
case RMIN:
case R:
case TRUE:
case NOT:
case LPARENTH:
case DLBRACKET:
case DLT:
case MINUS:
case DQUOTE:
case REG_INT:
case REG_DOUBLE:
case REG_IDENT:
expr = Expression(prop, true);
ret = expr;
break;
default:
jj_la1[85] = jj_gen;
@ -3658,12 +3684,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_67() {
if (jj_scan_token(COMMA)) return true;
if (jj_3R_28()) return true;
return false;
}
static private boolean jj_3R_113() {
if (jj_scan_token(LE)) return true;
return false;
@ -3674,13 +3694,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_136() {
if (jj_scan_token(LPARENTH)) return true;
if (jj_3R_39()) return true;
if (jj_scan_token(RPARENTH)) return true;
return false;
}
static private boolean jj_3R_111() {
if (jj_scan_token(LT)) return true;
return false;
@ -3707,13 +3720,21 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_105() {
if (jj_scan_token(NE)) return true;
static private boolean jj_3R_67() {
if (jj_scan_token(COMMA)) return true;
if (jj_3R_28()) return true;
return false;
}
static private boolean jj_3R_154() {
if (jj_scan_token(MAX)) return true;
static private boolean jj_3R_136() {
if (jj_scan_token(LPARENTH)) return true;
if (jj_3R_39()) return true;
if (jj_scan_token(RPARENTH)) return true;
return false;
}
static private boolean jj_3R_105() {
if (jj_scan_token(NE)) return true;
return false;
}
@ -3732,6 +3753,11 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_154() {
if (jj_scan_token(MAX)) return true;
return false;
}
static private boolean jj_3R_148() {
if (jj_scan_token(FALSE)) return true;
return false;
@ -3752,6 +3778,11 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_38() {
if (jj_scan_token(REG_IDENTPRIME)) return true;
return false;
}
static private boolean jj_3_3() {
if (jj_scan_token(LABEL)) return true;
if (jj_scan_token(DQUOTE)) return true;
@ -3763,8 +3794,8 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_38() {
if (jj_scan_token(REG_IDENTPRIME)) return true;
static private boolean jj_3R_180() {
if (jj_scan_token(OR)) return true;
return false;
}
@ -3773,11 +3804,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_180() {
if (jj_scan_token(OR)) return true;
return false;
}
static private boolean jj_3R_58() {
if (jj_scan_token(LPARENTH)) return true;
if (jj_3R_30()) return true;
@ -3842,6 +3868,11 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_31() {
if (jj_3R_28()) return true;
return false;
}
static private boolean jj_3R_152() {
if (jj_3R_39()) return true;
Token xsp;
@ -3860,8 +3891,13 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_31() {
if (jj_3R_28()) return true;
static private boolean jj_3R_179() {
if (jj_scan_token(AND)) return true;
return false;
}
static private boolean jj_3R_177() {
if (jj_scan_token(MAX)) return true;
return false;
}
@ -3872,13 +3908,13 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_179() {
if (jj_scan_token(AND)) return true;
static private boolean jj_3R_28() {
if (jj_scan_token(REG_IDENT)) return true;
return false;
}
static private boolean jj_3R_177() {
if (jj_scan_token(MAX)) return true;
static private boolean jj_3R_175() {
if (jj_scan_token(INIT)) return true;
return false;
}
@ -3922,13 +3958,9 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_28() {
if (jj_scan_token(REG_IDENT)) return true;
return false;
}
static private boolean jj_3R_175() {
if (jj_scan_token(INIT)) return true;
static private boolean jj_3R_182() {
if (jj_scan_token(COMMA)) return true;
if (jj_3R_39()) return true;
return false;
}
@ -3965,6 +3997,11 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_181() {
if (jj_3R_28()) return true;
return false;
}
static private boolean jj_3_8() {
if (jj_scan_token(OR)) return true;
if (jj_scan_token(OR)) return true;
@ -3976,9 +4013,18 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_182() {
if (jj_scan_token(COMMA)) return true;
if (jj_3R_39()) return true;
static private boolean jj_3R_178() {
if (jj_scan_token(PLUS)) return true;
return false;
}
static private boolean jj_3R_173() {
if (jj_3R_133()) return true;
return false;
}
static private boolean jj_3R_176() {
if (jj_scan_token(MIN)) return true;
return false;
}
@ -3995,18 +4041,13 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_181() {
static private boolean jj_3R_174() {
if (jj_3R_28()) return true;
return false;
}
static private boolean jj_3R_178() {
if (jj_scan_token(PLUS)) return true;
return false;
}
static private boolean jj_3R_173() {
if (jj_3R_133()) return true;
static private boolean jj_3R_171() {
if (jj_3R_139()) return true;
return false;
}
@ -4018,41 +4059,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_176() {
if (jj_scan_token(MIN)) return true;
return false;
}
static private boolean jj_3R_174() {
if (jj_3R_28()) return true;
return false;
}
static private boolean jj_3R_37() {
if (jj_scan_token(OR)) return true;
if (jj_scan_token(OR)) return true;
if (jj_3R_40()) return true;
return false;
}
static private boolean jj_3R_171() {
if (jj_3R_139()) return true;
return false;
}
static private boolean jj_3_10() {
if (jj_scan_token(OR)) return true;
if (jj_scan_token(LBRACKET)) return true;
return false;
}
static private boolean jj_3R_149() {
if (jj_scan_token(LPARENTH)) return true;
if (jj_3R_152()) return true;
if (jj_scan_token(RPARENTH)) return true;
return false;
}
static private boolean jj_3R_144() {
if (jj_scan_token(FILTER)) return true;
if (jj_scan_token(LPARENTH)) return true;
@ -4082,6 +4088,26 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_37() {
if (jj_scan_token(OR)) return true;
if (jj_scan_token(OR)) return true;
if (jj_3R_40()) return true;
return false;
}
static private boolean jj_3_10() {
if (jj_scan_token(OR)) return true;
if (jj_scan_token(LBRACKET)) return true;
return false;
}
static private boolean jj_3R_149() {
if (jj_scan_token(LPARENTH)) return true;
if (jj_3R_152()) return true;
if (jj_scan_token(RPARENTH)) return true;
return false;
}
static private boolean jj_3R_133() {
if (jj_3R_28()) return true;
Token xsp;
@ -4113,16 +4139,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_131() {
if (jj_3R_144()) return true;
return false;
}
static private boolean jj_3R_130() {
if (jj_3R_143()) return true;
return false;
}
static private boolean jj_3R_143() {
if (jj_scan_token(DQUOTE)) return true;
Token xsp;
@ -4135,6 +4151,16 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_131() {
if (jj_3R_144()) return true;
return false;
}
static private boolean jj_3R_130() {
if (jj_3R_143()) return true;
return false;
}
static private boolean jj_3R_129() {
if (jj_3R_142()) return true;
return false;
@ -4170,43 +4196,18 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_124() {
if (jj_3R_137()) return true;
return false;
}
static private boolean jj_3R_123() {
if (jj_3R_136()) return true;
return false;
}
static private boolean jj_3R_172() {
if (jj_3R_136()) return true;
return false;
}
static private boolean jj_3R_122() {
if (jj_3R_135()) return true;
return false;
}
static private boolean jj_3R_170() {
if (jj_3R_137()) return true;
return false;
}
static private boolean jj_3R_36() {
if (jj_3R_40()) return true;
Token xsp;
while (true) {
xsp = jj_scanpos;
if (jj_3R_41()) { jj_scanpos = xsp; break; }
}
return false;
}
static private boolean jj_3R_121() {
if (jj_3R_134()) return true;
static private boolean jj_3R_124() {
if (jj_3R_137()) return true;
return false;
}
@ -4216,8 +4217,8 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_120() {
if (jj_3R_133()) return true;
static private boolean jj_3R_123() {
if (jj_3R_136()) return true;
return false;
}
@ -4227,18 +4228,23 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_119() {
if (jj_3R_132()) return true;
static private boolean jj_3R_122() {
if (jj_3R_135()) return true;
return false;
}
static private boolean jj_3R_207() {
if (jj_3R_39()) return true;
static private boolean jj_3R_36() {
if (jj_3R_40()) return true;
Token xsp;
while (true) {
xsp = jj_scanpos;
if (jj_3R_41()) { jj_scanpos = xsp; break; }
}
return false;
}
static private boolean jj_3R_109() {
if (jj_scan_token(MINUS)) return true;
static private boolean jj_3R_121() {
if (jj_3R_134()) return true;
return false;
}
@ -4263,6 +4269,26 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_120() {
if (jj_3R_133()) return true;
return false;
}
static private boolean jj_3R_119() {
if (jj_3R_132()) return true;
return false;
}
static private boolean jj_3R_207() {
if (jj_3R_39()) return true;
return false;
}
static private boolean jj_3R_109() {
if (jj_scan_token(MINUS)) return true;
return false;
}
static private boolean jj_3R_118() {
Token xsp;
xsp = jj_scanpos;
@ -4317,6 +4343,14 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_141() {
if (jj_scan_token(A)) return true;
if (jj_scan_token(LBRACKET)) return true;
if (jj_3R_39()) return true;
if (jj_scan_token(RBRACKET)) return true;
return false;
}
static private boolean jj_3R_33() {
if (jj_3R_36()) return true;
Token xsp;
@ -4327,14 +4361,6 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_141() {
if (jj_scan_token(A)) return true;
if (jj_scan_token(LBRACKET)) return true;
if (jj_3R_39()) return true;
if (jj_scan_token(RBRACKET)) return true;
return false;
}
static private boolean jj_3R_106() {
Token xsp;
xsp = jj_scanpos;
@ -4374,6 +4400,14 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_140() {
if (jj_scan_token(E)) return true;
if (jj_scan_token(LBRACKET)) return true;
if (jj_3R_39()) return true;
if (jj_scan_token(RBRACKET)) return true;
return false;
}
static private boolean jj_3_1() {
if (jj_scan_token(MODULE)) return true;
if (jj_3R_28()) return true;
@ -4391,16 +4425,14 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_140() {
if (jj_scan_token(E)) return true;
if (jj_scan_token(LBRACKET)) return true;
if (jj_3R_39()) return true;
if (jj_scan_token(RBRACKET)) return true;
static private boolean jj_3_16() {
if (jj_scan_token(DQUOTE)) return true;
return false;
}
static private boolean jj_3_16() {
if (jj_scan_token(DQUOTE)) return true;
static private boolean jj_3_17() {
if (jj_scan_token(C)) return true;
if (jj_scan_token(LE)) return true;
return false;
}
@ -4409,9 +4441,8 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3_17() {
if (jj_scan_token(C)) return true;
if (jj_scan_token(LE)) return true;
static private boolean jj_3R_201() {
if (jj_3R_39()) return true;
return false;
}
@ -4431,21 +4462,8 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_209() {
if (jj_scan_token(DQUOTE)) return true;
if (jj_3R_28()) return true;
if (jj_scan_token(DQUOTE)) return true;
return false;
}
static private boolean jj_3R_201() {
if (jj_scan_token(S)) return true;
return false;
}
static private boolean jj_3R_200() {
if (jj_scan_token(F)) return true;
if (jj_3R_39()) return true;
if (jj_scan_token(S)) return true;
return false;
}
@ -4461,7 +4479,9 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3_15() {
static private boolean jj_3R_209() {
if (jj_scan_token(DQUOTE)) return true;
if (jj_3R_28()) return true;
if (jj_scan_token(DQUOTE)) return true;
return false;
}
@ -4473,13 +4493,8 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_98() {
if (jj_3R_101()) return true;
Token xsp;
while (true) {
xsp = jj_scanpos;
if (jj_3R_102()) { jj_scanpos = xsp; break; }
}
static private boolean jj_3_15() {
if (jj_scan_token(DQUOTE)) return true;
return false;
}
@ -4502,6 +4517,16 @@ public class PrismParser implements PrismParserConstants {
return false;
}
static private boolean jj_3R_98() {
if (jj_3R_101()) return true;
Token xsp;
while (true) {
xsp = jj_scanpos;
if (jj_3R_102()) { jj_scanpos = xsp; break; }
}
return false;
}
static private boolean jj_3_6() {
if (jj_scan_token(DQUOTE)) return true;
return false;
@ -4906,13 +4931,13 @@ public class PrismParser implements PrismParserConstants {
jj_la1_init_2();
}
private static void jj_la1_init_0() {
jj_la1_0 = new int[] {0x514404c0,0x504404c0,0x1000000,0xb01a0848,0x0,0xb01a0848,0xb01a0848,0x0,0xb01a0848,0x400,0x40000000,0x80,0x40000480,0x8000210,0x8000210,0x0,0x40,0x0,0x1000000,0x8000030,0x0,0x2000000,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0xa00000,0x0,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0xa01a0808,0x0,0xa0000000,0xa0000000,0x0,0x20000,0x0,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0x0,0x0,0x0,0xa0000000,0x0,0x0,0xa0ba0808,0xa0ba0808,0x0,0x4200100,0x0,0x0,0x1000000,0xa0000000,0x0,0xa0000000,0x0,0x0,0x0,};
jj_la1_0 = new int[] {0x514404c0,0x504404c0,0x1000000,0xb01a0848,0x0,0xb01a0848,0xb01a0848,0x0,0xb01a0848,0x400,0x40000000,0x80,0x40000480,0x8000210,0x8000210,0x0,0x40,0x0,0x1000000,0x8000030,0x0,0x2000000,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0xa00000,0x0,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0xa0ba0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0x0,0x0,0x0,0x0,0x0,0x0,0xa01a0808,0xa01a0808,0x0,0xa0000000,0xa0000000,0x0,0x20000,0x0,0xa0000000,0x0,0x0,0x0,0xa0000000,0x0,0x0,0x0,0x0,0x0,0xa0000000,0x0,0x0,0xa0ba0808,0xa0ba0808,0x0,0xa4ba0908,0x0,0x0,0x1000000,0xa0000000,0x0,0xa0000000,0x0,0x0,0x0,};
}
private static void jj_la1_init_1() {
jj_la1_1 = new int[] {0x187c5,0x83c4,0x10401,0x40127ab8,0x8000000,0x40127ab8,0x40127ab8,0x8000000,0x40127ab8,0x40,0x4,0x8000,0x8144,0x0,0x0,0x280,0x280,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x4012783a,0x200000,0x40020000,0x10000000,0x4012783a,0x0,0x0,0x10000000,0x0,0x10000000,0x10000000,0x0,0x40000000,0xc2000,0x0,0xc2000,0x2,0x0,0x4012783a,0x4012783a,0x4012783a,0x4012783a,0x4012783a,0x0,0x0,0x800000,0x1000000,0x400000,0x200000,0x40127838,0x0,0x0,0x0,0x0,0x0,0x0,0x40027838,0x40027838,0x40000000,0x0,0x0,0x10000000,0x20000,0x40000000,0x0,0x38,0x0,0x0,0x0,0x40000000,0x40000000,0x0,0x40000000,0x0,0x0,0x3800,0x0,0x4012783a,0x4012783a,0x0,0x4000,0x0,0x40003838,0x0,0x600000,0x10000000,0x0,0x0,0x0,0x4000000,};
jj_la1_1 = new int[] {0x187c5,0x83c4,0x10401,0x40127ab8,0x8000000,0x40127ab8,0x40127ab8,0x8000000,0x40127ab8,0x40,0x4,0x8000,0x8144,0x0,0x0,0x280,0x280,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x4012783a,0x200000,0x40020000,0x10000000,0x4012783a,0x0,0x0,0x10000000,0x0,0x10000000,0x10000000,0x0,0x40000000,0xc2000,0x0,0xc2000,0x2,0x0,0x4012783a,0x4012783a,0x4012783a,0x4012783a,0x4012783a,0x0,0x0,0x800000,0x1000000,0x400000,0x200000,0x40127838,0x0,0x0,0x0,0x0,0x0,0x0,0x40027838,0x40027838,0x40000000,0x0,0x0,0x10000000,0x20000,0x40000000,0x0,0x38,0x0,0x0,0x0,0x40000000,0x40000000,0x0,0x40000000,0x0,0x0,0x3800,0x0,0x4012783a,0x4012783a,0x0,0x4012783a,0x0,0x40003838,0x0,0x600000,0x10000000,0x0,0x0,0x0,0x4000000,};
}
private static void jj_la1_init_2() {
jj_la1_2 = new int[] {0x0,0x0,0x0,0x2e08404,0x0,0x2e08404,0x2e08404,0x0,0x2e08404,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x40,0x0,0x1,0x2000000,0x0,0x1,0x2000000,0x4000,0x2e08404,0x0,0x0,0x0,0x2e08405,0x2000000,0x1,0x0,0x20010,0x0,0x0,0x20010,0x2200000,0x0,0x3341,0x0,0x0,0x3341,0x2e08404,0x2e08404,0x2e08404,0x2e08404,0x2e08404,0x3341,0x100000,0x0,0x0,0x0,0x0,0x2e08404,0xc0,0x3300,0xc000,0xc000,0x30000,0x30000,0x2e08404,0x2e00404,0x0,0x0,0x2000000,0x0,0xc00000,0x0,0x3340,0x0,0x10,0x10,0x0,0x0,0x3340,0x10,0x0,0x10,0x3340,0x0,0x10,0x2e08404,0x2e08404,0x20000,0x0,0x404,0x2000000,0x2000000,0x2004000,0x0,0x2000000,0xc0,0x3300,0x0,};
jj_la1_2 = new int[] {0x0,0x0,0x0,0x2e08404,0x0,0x2e08404,0x2e08404,0x0,0x2e08404,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x0,0x40,0x0,0x1,0x2000000,0x0,0x1,0x2000000,0x4000,0x2e08404,0x0,0x0,0x0,0x2e08405,0x2000000,0x1,0x0,0x20010,0x0,0x0,0x20010,0x2200000,0x0,0x3341,0x0,0x0,0x3341,0x2e08404,0x2e08404,0x2e08404,0x2e08404,0x2e08404,0x3341,0x100000,0x0,0x0,0x0,0x0,0x2e08404,0xc0,0x3300,0xc000,0xc000,0x30000,0x30000,0x2e08404,0x2e00404,0x0,0x0,0x2000000,0x0,0xc00000,0x0,0x3340,0x0,0x10,0x10,0x0,0x0,0x3340,0x10,0x0,0x10,0x3340,0x0,0x10,0x2e08404,0x2e08404,0x20000,0x2e08404,0x404,0x2000000,0x2000000,0x2004000,0x0,0x2000000,0xc0,0x3300,0x0,};
}
static final private JJCalls[] jj_2_rtns = new JJCalls[17];
static private boolean jj_rescan = false;

18
prism/src/parser/PrismParser.jj
View File

@ -1632,15 +1632,21 @@ void RewardIndex(ExpressionReward exprRew) :
Expression ExpressionRewardContents(boolean prop, boolean pathprop) :
{
Expression expr = null;
ExpressionTemporal ret = null;
ExpressionTemporal exprTemp = null;
Expression ret = null;
Token begin;
}
{
( LOOKAHEAD(<C> <LE>) begin = <C> <LE> expr = Expression(false, false) { ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); ret.setUpperBound(expr); }
| begin = <C> { ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); }
| begin = <I> <EQ> expr = Expression(false, false) { ret = new ExpressionTemporal(ExpressionTemporal.R_I, null, null); ret.setUpperBound(expr); }
| begin = <F> expr = Expression(prop, pathprop) { ret = new ExpressionTemporal(ExpressionTemporal.R_F, null, expr); }
| begin = <S> { ret = new ExpressionTemporal(ExpressionTemporal.R_S, null, null); } )
{ begin = getToken(1); }
(
// Normal reward operators
LOOKAHEAD(<C> <LE>) begin = <C> <LE> expr = Expression(false, false) { exprTemp = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); exprTemp.setUpperBound(expr); ret = exprTemp; }
| <C> { ret = new ExpressionTemporal(ExpressionTemporal.R_C, null, null); }
| <I> <EQ> expr = Expression(false, false) { exprTemp = new ExpressionTemporal(ExpressionTemporal.R_I, null, null); exprTemp.setUpperBound(expr); ret = exprTemp; }
| <S> { ret = new ExpressionTemporal(ExpressionTemporal.R_S, null, null); }
// Path formula (including F "target")
| expr = Expression(prop, true) { ret = expr; }
)
{ ret.setPosition(begin, getToken(0)); return ret; }
}

3
prism/src/parser/visitor/TypeCheck.java
View File

@ -516,7 +516,8 @@ public class TypeCheck extends ASTTraverse
}
}
// Check argument
if (!(e.getExpression().getType() instanceof TypePathDouble)) {
Type typeArg = e.getExpression().getType();
if (!(typeArg instanceof TypePathDouble || typeArg instanceof TypePathBool || typeArg instanceof TypeBool)) {
throw new PrismLangException("Type error: Contents of R operator is invalid", e.getExpression());
}
// Set type

218
prism/src/prism/NondetModelChecker.java
View File

@ -29,27 +29,44 @@
package prism;
import hybrid.PrismHybrid;
import java.io.File;
import java.io.FileNotFoundException;
import java.util.*;
import java.util.ArrayList;
import java.util.BitSet;
import java.util.List;
import java.util.Vector;
import jdd.JDD;
import jdd.JDDNode;
import jdd.JDDVars;
import mtbdd.PrismMTBDD;
import odd.ODDUtils;
import parser.ast.Expression;
import parser.ast.ExpressionFunc;
import parser.ast.ExpressionProb;
import parser.ast.ExpressionQuant;
import parser.ast.ExpressionReward;
import parser.ast.ExpressionTemporal;
import parser.ast.ExpressionUnaryOp;
import parser.ast.PropertiesFile;
import parser.ast.RelOp;
import parser.type.TypeBool;
import parser.type.TypePathBool;
import parser.type.TypePathDouble;
import sparse.PrismSparse;
import strat.MDStrategyIV;
import acceptance.AcceptanceOmega;
import acceptance.AcceptanceOmegaDD;
import acceptance.AcceptanceRabin;
import acceptance.AcceptanceRabinDD;
import acceptance.AcceptanceReachDD;
import acceptance.AcceptanceType;
import automata.DA;
import automata.LTL2DA;
import odd.ODDUtils;
import jdd.*;
import dv.*;
import dv.DoubleVector;
import dv.IntegerVector;
import explicit.MinMax;
import mtbdd.*;
import sparse.*;
import strat.MDStrategyIV;
import hybrid.*;
import parser.ast.*;
/*
* Model checker for MDPs
@ -219,7 +236,7 @@ public class NondetModelChecker extends NonProbModelChecker
// Compute rewards
StateValues rewards = null;
Expression expr2 = expr.getExpression();
if (expr2 instanceof ExpressionTemporal) {
if (expr2.getType() instanceof TypePathDouble) {
ExpressionTemporal exprTemp = (ExpressionTemporal) expr2;
switch (exprTemp.getOperator()) {
case ExpressionTemporal.R_C:
@ -236,7 +253,10 @@ public class NondetModelChecker extends NonProbModelChecker
rewards = checkRewardReach(exprTemp, stateRewards, transRewards, minMax.isMin());
break;
}
} else if (expr2.getType() instanceof TypePathBool || expr2.getType() instanceof TypeBool) {
rewards = checkRewardPathFormula(expr2, stateRewards, transRewards, minMax.isMin());
}
if (rewards == null)
throw new PrismException("Unrecognised operator in R operator");
@ -339,6 +359,7 @@ public class NondetModelChecker extends NonProbModelChecker
modelProduct = model;
// Go through probabilistic objectives and construct product MDP.
long l = System.currentTimeMillis();
boolean originalmodel = true;
for (int i = 0; i < numObjectives; i++) {
if (opsAndBounds.isProbabilityObjective(i)) {
@ -354,6 +375,8 @@ public class NondetModelChecker extends NonProbModelChecker
originalmodel = false;
}
}
l = System.currentTimeMillis() - l;
mainLog.println("Total time for product construction: " + l / 1000.0 + " seconds.");
// TODO: move this above
// Replace min by max and <= by >=
@ -1030,6 +1053,8 @@ public class NondetModelChecker extends NonProbModelChecker
daDDRowVars = new JDDVars();
daDDColVars = new JDDVars();
modelProduct = mcLtl.constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars);
l = System.currentTimeMillis() - l;
mainLog.println("Time for product construction: " + l / 1000.0 + " seconds.");
mainLog.println();
modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo());
// Output product, if required
@ -1159,6 +1184,19 @@ public class NondetModelChecker extends NonProbModelChecker
/**
* Compute rewards for a reachability reward operator.
*/
protected StateValues checkRewardPathFormula(Expression expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
{
if (expr instanceof ExpressionTemporal && ((ExpressionTemporal) expr).getOperator() == ExpressionTemporal.P_F){
return checkRewardReach((ExpressionTemporal) expr, stateRewards, transRewards, min);
}
else if (Expression.isCoSafeLTLSyntactic(expr)) {
return checkRewardCoSafeLTL(expr, stateRewards, transRewards, min);
}
throw new PrismException("Invalid contents for an R operator: " + expr);
}
// reach reward
protected StateValues checkRewardReach(ExpressionTemporal expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
{
JDDNode b;
@ -1185,6 +1223,150 @@ public class NondetModelChecker extends NonProbModelChecker
return rewards;
}
// co-safe LTL reward
protected StateValues checkRewardCoSafeLTL(Expression expr, JDDNode stateRewards, JDDNode transRewards, boolean min) throws PrismException
{
LTLModelChecker mcLtl;
StateValues rewardsProduct = null, rewards = null;
Expression ltl;
Vector<JDDNode> labelDDs;
DA<BitSet, ? extends AcceptanceOmega> da;
NondetModel modelProduct;
NondetModelChecker mcProduct;
JDDNode startMask;
JDDVars daDDRowVars, daDDColVars;
int i;
long l;
if (Expression.containsTemporalTimeBounds(expr)) {
if (model.getModelType().continuousTime()) {
throw new PrismException("DA construction for time-bounded operators not supported for " + model.getModelType()+".");
}
if (expr.isSimplePathFormula()) {
// Convert simple path formula to canonical form,
// DA is then generated by LTL2RabinLibrary.
//
// The conversion to canonical form has to happen here, because once
// checkMaximalStateFormulas has been called, the formula should not be modified
// anymore, as converters may expect that the generated labels for maximal state
// formulas only appear positively
expr = Expression.convertSimplePathFormulaToCanonicalForm(expr);
} else {
throw new PrismException("Time-bounded operators not supported in LTL: " + expr);
}
}
// Can't do "dfa" properties yet
if (expr instanceof ExpressionFunc && ((ExpressionFunc) expr).getName().equals("dfa")) {
throw new PrismException("Model checking for \"dfa\" specifications not supported yet");
}
// For LTL model checking routines
mcLtl = new LTLModelChecker(prism);
// Model check maximal state formulas
labelDDs = new Vector<JDDNode>();
ltl = mcLtl.checkMaximalStateFormulas(this, model, expr.deepCopy(), labelDDs);
// Convert LTL formula to deterministic automaton (DA)
mainLog.println("\nBuilding deterministic automaton (for " + ltl + ")...");
l = System.currentTimeMillis();
LTL2DA ltl2da = new LTL2DA(prism);
AcceptanceType[] allowedAcceptance = {
AcceptanceType.RABIN,
AcceptanceType.REACH
};
da = ltl2da.convertLTLFormulaToDA(ltl, constantValues, allowedAcceptance);
mainLog.println(da.getAutomataType()+" has " + da.size() + " states, " + da.getAcceptance().getSizeStatistics()+".");
l = System.currentTimeMillis() - l;
mainLog.println("Time for deterministic automaton translation: " + l / 1000.0 + " seconds.");
// If required, export DA
if (prism.getSettings().getExportPropAut()) {
mainLog.println("Exporting DA to file \"" + prism.getSettings().getExportPropAutFilename() + "\"...");
PrismLog out = new PrismFileLog(prism.getSettings().getExportPropAutFilename());
da.print(out, prism.getSettings().getExportPropAutType());
out.close();
//da.printDot(new java.io.PrintStream("da.dot"));
}
// Build product of MDP and automaton
mainLog.println("\nConstructing MDP-"+da.getAutomataType()+" product...");
daDDRowVars = new JDDVars();
daDDColVars = new JDDVars();
l = System.currentTimeMillis();
modelProduct = mcLtl.constructProductMDP(da, model, labelDDs, daDDRowVars, daDDColVars);
l = System.currentTimeMillis() - l;
mainLog.println("Time for product construction: " + l / 1000.0 + " seconds.");
mainLog.println();
modelProduct.printTransInfo(mainLog, prism.getExtraDDInfo());
// Output product, if required
if (prism.getExportProductTrans()) {
try {
mainLog.println("\nExporting product transition matrix to file \"" + prism.getExportProductTransFilename() + "\"...");
modelProduct.exportToFile(Prism.EXPORT_PLAIN, true, new File(prism.getExportProductTransFilename()));
} catch (FileNotFoundException e) {
mainLog.printWarning("Could not export product transition matrix to file \"" + prism.getExportProductTransFilename() + "\"");
}
}
if (prism.getExportProductStates()) {
mainLog.println("\nExporting product state space to file \"" + prism.getExportProductStatesFilename() + "\"...");
PrismFileLog out = new PrismFileLog(prism.getExportProductStatesFilename());
modelProduct.exportStates(Prism.EXPORT_PLAIN, out);
out.close();
}
// Adapt reward info to product model
JDD.Ref(stateRewards);
JDD.Ref(modelProduct.getReach());
JDDNode stateRewardsProduct = JDD.Apply(JDD.TIMES, stateRewards, modelProduct.getReach());
JDD.Ref(transRewards);
JDD.Ref(modelProduct.getTrans01());
JDDNode transRewardsProduct = JDD.Apply(JDD.TIMES, transRewards, modelProduct.getTrans01());
// Find accepting states + compute reachability rewards
AcceptanceOmegaDD acceptance = da.getAcceptance().toAcceptanceDD(daDDRowVars);
JDDNode acc = null;
if (acceptance instanceof AcceptanceReachDD) {
// For a DFA, just collect the accept states
mainLog.println("\nSkipping end component detection since DRA is a DFA...");
acc = ((AcceptanceReachDD) acceptance).getGoalStates();
} else {
// Usually, we have to detect end components in the product
mainLog.println("\nFinding accepting end components...");
acc = mcLtl.findAcceptingECStates(acceptance, modelProduct, daDDRowVars, daDDColVars, fairness);
}
acceptance.clear();
mainLog.println("\nComputing reachability rewards...");
mcProduct = new NondetModelChecker(prism, modelProduct, null);
rewardsProduct = mcProduct.computeReachRewards(modelProduct.getTrans(), modelProduct.getTransActions(), modelProduct.getTrans01(), stateRewardsProduct, transRewardsProduct, acc, min);
// Convert reward vector to original model
// First, filter over DRA start states
startMask = mcLtl.buildStartMask(da, labelDDs, daDDRowVars);
JDD.Ref(model.getReach());
startMask = JDD.And(model.getReach(), startMask);
rewardsProduct.filter(startMask);
// Then sum over DD vars for the DRA state
rewards = rewardsProduct.sumOverDDVars(daDDRowVars, model);
// Deref, clean up
JDD.Deref(stateRewardsProduct);
JDD.Deref(transRewardsProduct);
rewardsProduct.clear();
modelProduct.clear();
for (i = 0; i < labelDDs.size(); i++) {
JDD.Deref(labelDDs.get(i));
}
JDD.Deref(acc);
JDD.Deref(startMask);
daDDRowVars.derefAll();
daDDColVars.derefAll();
return rewards;
}
// -----------------------------------------------------------------------------------
// probability computation methods
// -----------------------------------------------------------------------------------
@ -1683,6 +1865,18 @@ public class NondetModelChecker extends NonProbModelChecker
List<JDDNode> zeroCostEndComponents = null;
// If required, export info about target states
if (prism.getExportTarget()) {
JDDNode labels[] = { model.getStart(), b };
String labelNames[] = { "init", "target" };
try {
mainLog.println("\nExporting target states info to file \"" + prism.getExportTargetFilename() + "\"...");
PrismMTBDD.ExportLabels(labels, labelNames, "l", model.getAllDDRowVars(), model.getODD(), Prism.EXPORT_PLAIN, prism.getExportTargetFilename());
} catch (FileNotFoundException e) {
mainLog.printWarning("Could not export target to file \"" + prism.getExportTargetFilename() + "\"");
}
}
// compute states which can't reach goal with probability 1
if (b.equals(JDD.ZERO)) {
JDD.Ref(reach);

Write Preview
Loading…
Cancel
Save