From 2f749bd92e1c8b2d99fecad582f421de81dac3a0 Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Fri, 12 Oct 2018 14:25:03 +0200 Subject: [PATCH] imported patch symb-common-symb-LTLMC-lift-reward.patch --- prism/src/prism/LTLModelChecker.java | 32 ++++++++++++++++++++++++---- 1 file changed, 28 insertions(+), 4 deletions(-) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index fffcc145..fafb8454 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -547,12 +547,24 @@ public class LTLModelChecker extends PrismComponent newStart = buildStartMask(da, labelDDs, daDDRowVars); newStart = JDD.And(model.getReach().copy(), statesOfInterest.copy(), newStart); + // Build lifted reward information + JDDNode[] newStateRewards = new JDDNode[model.stateRewards.length]; + for (i=0; i < model.stateRewards.length; i++) { + newStateRewards[i] = model.stateRewards[i].copy(); + } + JDDNode[] newTransRewards = new JDDNode[model.transRewards.length]; + for (i=0; i < model.transRewards.length; i++) { + newTransRewards[i] = model.transRewards[i].copy(); + } + // Create a new model model object to store the product model ProbModel modelProd = new ProbModel( // New transition matrix/start state newTrans, newStart, - // Don't pass in any rewards info - new JDDNode[0], new JDDNode[0], new String[0], + // lifted rewards info + newStateRewards, + newTransRewards, + model.rewardStructNames.clone(), // New list of all row/col vars newAllDDRowVars, newAllDDColVars, // New model variables @@ -839,12 +851,24 @@ public class LTLModelChecker extends PrismComponent newStart = buildStartMask(da, labelDDs, daDDRowVars); newStart = JDD.And(model.getReach().copy(), statesOfInterest.copy(), newStart); + // Build lifted reward information + JDDNode[] newStateRewards = new JDDNode[model.stateRewards.length]; + for (i=0; i < model.stateRewards.length; i++) { + newStateRewards[i] = model.stateRewards[i].copy(); + } + JDDNode[] newTransRewards = new JDDNode[model.transRewards.length]; + for (i=0; i < model.transRewards.length; i++) { + newTransRewards[i] = model.transRewards[i].copy(); + } + // Create a new model model object to store the product model NondetModel modelProd = new NondetModel( // New transition matrix/start state newTrans, newStart, - // Don't pass in any rewards info - new JDDNode[0], new JDDNode[0], new String[0], + // lifted rewards info + newStateRewards, + newTransRewards, + model.rewardStructNames.clone(), // New list of all row/col vars newAllDDRowVars, newAllDDColVars, // Nondet variables (unchanged)