diff --git a/prism-examples/pomdps/simple/guess-multi.prism b/prism-examples/pomdps/simple/guess-multi.prism index a8f50124ad..412af711d1 100644 --- a/prism-examples/pomdps/simple/guess-multi.prism +++ b/prism-examples/pomdps/simple/guess-multi.prism @@ -9,7 +9,7 @@ observables s, g endobservables module M - s : [0..2]; // state + s : [0..3]; // state h : [0..3]; // hidden var g : [0..N] init N; // num guesses left diff --git a/prism-examples/pomdps/simple/guess.prism b/prism-examples/pomdps/simple/guess.prism index 8a1c849969..961f8bd540 100644 --- a/prism-examples/pomdps/simple/guess.prism +++ b/prism-examples/pomdps/simple/guess.prism @@ -6,7 +6,7 @@ observables s endobservables module M - s : [0..2]; // state + s : [0..3]; // state h : [0..3]; // hidden var // Assign hidden variable randomly diff --git a/prism-tests/functionality/export/pomdp/maze.prism.tra b/prism-tests/functionality/export/pomdp/maze.prism.tra index 28ba0c90ec..d2dc613729 100644 --- a/prism-tests/functionality/export/pomdp/maze.prism.tra +++ b/prism-tests/functionality/export/pomdp/maze.prism.tra @@ -1,4 +1,5 @@ 12 21 30 8 +- - 0 - 0 0 0 1 0.1 1 0 0 2 0.1 2 0 0 3 0.1 3 diff --git a/prism-tests/functionality/import/maze.lab b/prism-tests/functionality/import/maze.lab new file mode 100644 index 0000000000..66d575da37 --- /dev/null +++ b/prism-tests/functionality/import/maze.lab @@ -0,0 +1,2 @@ +0="init" 1="deadlock" +0: 0 diff --git a/prism-tests/functionality/import/maze.obs b/prism-tests/functionality/import/maze.obs new file mode 100644 index 0000000000..4726575a7c --- /dev/null +++ b/prism-tests/functionality/import/maze.obs @@ -0,0 +1,9 @@ +(west,east,north,south,target) +0:(false,false,false,false,false) +1:(true,false,true,false,false) +2:(false,false,true,true,false) +3:(false,false,true,false,false) +4:(false,true,true,false,false) +5:(true,true,false,false,false) +6:(true,true,false,true,false) +7:(true,true,false,true,true) diff --git a/prism-tests/functionality/import/maze.prism.importexport.auto b/prism-tests/functionality/import/maze.prism.importexport.auto new file mode 100644 index 0000000000..eff3da3653 --- /dev/null +++ b/prism-tests/functionality/import/maze.prism.importexport.auto @@ -0,0 +1 @@ +-importmodel maze.all -exportmodel maze.all diff --git a/prism-tests/functionality/import/maze.prism.orig b/prism-tests/functionality/import/maze.prism.orig new file mode 100644 index 0000000000..9f68874d7c --- /dev/null +++ b/prism-tests/functionality/import/maze.prism.orig @@ -0,0 +1,84 @@ +// maze example (POMDP) +// Littman, Cassandra and Kaelbling +// Learning policies for partially observable environments: Scaling up +// Technical Report CS, Brown University +// gxn 29/01/16 + +// state space (value of variable "s") + +// 0 1 2 3 4 +// 5 6 7 +// 8 10 9 + +// 10 is the target + +pomdp + +// can observe the walls and target +observable "west" = s=0|s=5|s=6|s=7|s=8|s=9|s=10; // wall to the west +observable "east" = s=4|s=5|s=6|s=7|s=8|s=9|s=10; // wall to the east +observable "north" = s=0|s=1|s=2|s=3|s=4; // wall to the north +observable "south" = s=1|s=3|s=8|s=9|s=10; // wall to the south +observable "target" = s=10; //target + +module maze + + s : [-1..10]; + + // initialisation + [] s=-1 -> 0.1 : (s'=0) + + 0.1 : (s'=1) + + 0.1 : (s'=2) + + 0.1 : (s'=3) + + 0.1 : (s'=4) + + 0.1 : (s'=5) + + 0.1 : (s'=6) + + 0.1 : (s'=7) + + 0.1 : (s'=8) + + 0.1 : (s'=9); + + // moving around the maze + + [east] s=0 -> (s'=1); + [south] s=0 -> (s'=5); + + [east] s=1 -> (s'=2); + [west] s=1 -> (s'=0); + + [east] s=2 -> (s'=3); + [west] s=2 -> (s'=1); + [south] s=2 -> (s'=6); + + [east] s=3 -> (s'=4); + [west] s=3 -> (s'=2); + + [west] s=4 -> (s'=3); + [south] s=4 -> (s'=7); + + [north] s=5 -> (s'=0); + [south] s=5 -> (s'=8); + + [north] s=6 -> (s'=2); + [south] s=6 -> (s'=10); + + [north] s=7 -> (s'=4); + [south] s=7 -> (s'=9); + + [north] s=8 -> (s'=5); + + [north] s=9 -> (s'=7); + + // loop when we reach the target + [done] s=10 -> true; + +endmodule + +// reward structure (number of steps to reach the target) +rewards + + [east] true : 1; + [west] true : 1; + [north] true : 1; + [south] true : 1; + +endrewards diff --git a/prism-tests/functionality/import/maze.srew b/prism-tests/functionality/import/maze.srew new file mode 100644 index 0000000000..77f5cea872 --- /dev/null +++ b/prism-tests/functionality/import/maze.srew @@ -0,0 +1,3 @@ +# Reward structure +# State rewards +12 0 diff --git a/prism-tests/functionality/import/maze.sta b/prism-tests/functionality/import/maze.sta new file mode 100644 index 0000000000..7f3b0b0884 --- /dev/null +++ b/prism-tests/functionality/import/maze.sta @@ -0,0 +1,13 @@ +(s) +0:(-1) +1:(0) +2:(1) +3:(2) +4:(3) +5:(4) +6:(5) +7:(6) +8:(7) +9:(8) +10:(9) +11:(10) diff --git a/prism-tests/functionality/import/maze.tra b/prism-tests/functionality/import/maze.tra new file mode 100644 index 0000000000..d2dc613729 --- /dev/null +++ b/prism-tests/functionality/import/maze.tra @@ -0,0 +1,32 @@ +12 21 30 8 +- - 0 - 0 +0 0 1 0.1 1 +0 0 2 0.1 2 +0 0 3 0.1 3 +0 0 4 0.1 2 +0 0 5 0.1 4 +0 0 6 0.1 5 +0 0 7 0.1 5 +0 0 8 0.1 5 +0 0 9 0.1 6 +0 0 10 0.1 6 +1 0 2 1 2 east +1 1 6 1 5 south +2 0 3 1 3 east +2 1 1 1 1 west +3 0 4 1 2 east +3 1 7 1 5 south +3 2 2 1 2 west +4 0 5 1 4 east +4 1 3 1 3 west +5 0 8 1 5 south +5 1 4 1 2 west +6 0 9 1 6 south +6 1 1 1 1 north +7 0 11 1 7 south +7 1 3 1 3 north +8 0 10 1 6 south +8 1 5 1 4 north +9 0 6 1 5 north +10 0 8 1 5 north +11 0 11 1 7 done diff --git a/prism-tests/functionality/import/maze.trew b/prism-tests/functionality/import/maze.trew new file mode 100644 index 0000000000..337fa4ead1 --- /dev/null +++ b/prism-tests/functionality/import/maze.trew @@ -0,0 +1,22 @@ +# Reward structure +# Transition rewards +12 21 19 +1 0 2 1 +1 1 6 1 +2 0 3 1 +2 1 1 1 +3 0 4 1 +3 1 7 1 +3 2 2 1 +4 0 5 1 +4 1 3 1 +5 0 8 1 +5 1 4 1 +6 0 9 1 +6 1 1 1 +7 0 11 1 +7 1 3 1 +8 0 10 1 +8 1 5 1 +9 0 6 1 +10 0 8 1 diff --git a/prism-tests/functionality/verify/pomdps/guess-multi.prism b/prism-tests/functionality/verify/pomdps/guess-multi.prism index d3a2306d84..d0d9fb3cff 100644 --- a/prism-tests/functionality/verify/pomdps/guess-multi.prism +++ b/prism-tests/functionality/verify/pomdps/guess-multi.prism @@ -4,7 +4,7 @@ const int N; module M - s : [0..2]; // state + s : [0..3]; // state h : [0..3]; // hidden var g : [0..N] init N; // num guesses left diff --git a/prism-tests/functionality/verify/pomdps/guess.prism b/prism-tests/functionality/verify/pomdps/guess.prism index d41bed39d6..fbf6b8237c 100644 --- a/prism-tests/functionality/verify/pomdps/guess.prism +++ b/prism-tests/functionality/verify/pomdps/guess.prism @@ -4,7 +4,7 @@ const double p = 0.2; module M - s : [0..2]; // state + s : [0..3]; // state h : [0..3]; // hidden var [toss] s=0 -> 0.1:(s'=1)&(h'=1) + 0.3:(s'=1)&(h'=2) + 0.6:(s'=1)&(h'=3); diff --git a/prism/src/explicit/ExplicitFiles2Model.java b/prism/src/explicit/ExplicitFiles2Model.java index 224b63955f..43fbeab7ab 100644 --- a/prism/src/explicit/ExplicitFiles2Model.java +++ b/prism/src/explicit/ExplicitFiles2Model.java @@ -112,6 +112,10 @@ public Model build(ExplicitModelImporter modelImporter, Evaluator MDP mdp = isDbl ? (MDP) new MDPSparse() : new MDPSimple<>(); model = (ModelExplicit) mdp; break; + case POMDP: + POMDP pomdp = new POMDPSimple<>(); + model = (ModelExplicit) pomdp; + break; case IDTMC: IDTMCSimple idtmc = new IDTMCSimple<>(); model = (ModelExplicit) idtmc; @@ -159,6 +163,9 @@ public Model build(ExplicitModelImporter modelImporter, Evaluator } loadStates(modelImporter, model); + if (model.getModelType().partiallyObservable()) { + loadObservationDefinitions(modelImporter, (POMDPSimple) model); + } return model; } @@ -196,7 +203,28 @@ private void loadStates(ExplicitModelImporter modelImporter, ModelExplicit mo for (int i = 0; i < numStates; i++) { statesList.add(new State(numVars)); } - modelImporter.extractStates((s, i, o) -> statesList.get(s).setValue(i, o)); + modelImporter.extractStates((s, i, v) -> statesList.get(s).setValue(i, v)); model.setStatesList(statesList); } + + /** + * Load the observation information, and store in model + */ + private void loadObservationDefinitions(ExplicitModelImporter modelImporter, POMDPSimple model) throws PrismException + { + int numObservations = model.getNumObservations(); + int numObservables = modelImporter.getModelInfo().getNumObservables(); + List observationsList = new ArrayList<>(numObservations); + for (int i = 0; i < numObservations; i++) { + observationsList.add(new State(numObservables)); + } + modelImporter.extractObservationDefinitions((o, i, v) -> observationsList.get(o).setValue(i, v)); + model.setObservationsList(observationsList); + List statesList = model.getStatesList(); + if (statesList != null) { + model.setUnobservationsList(new ArrayList<>(statesList)); + } else { + throw new PrismException("Can't load observation definitions without a states list"); + } + } } diff --git a/prism/src/explicit/ObservationsSimple.java b/prism/src/explicit/ObservationsSimple.java index 7a67ff71d7..debf3b2153 100644 --- a/prism/src/explicit/ObservationsSimple.java +++ b/prism/src/explicit/ObservationsSimple.java @@ -83,16 +83,19 @@ public ObservationsSimple() */ public ObservationsSimple(int numStates) { - this.numStates = numStates; - observationsList = new ArrayList<>(); - unobservationsList = new ArrayList<>(); - observationStates = new ArrayList<>(); - observablesMap = new ArrayList<>(); - unobservablesMap = new ArrayList<>(); - for (int i = 0; i < numStates; i++) { - observablesMap.add(-1); - unobservablesMap.add(-1); - } + this(); + addStates(numStates); + } + + /** + * Constructor: initialise storage for observable info when the model has + * {@code numStates} states and {@code numObservations} observations. + */ + public ObservationsSimple(int numStates, int numObservations) + { + this(); + addStates(numStates); + addObservations(numObservations); } /** @@ -137,6 +140,17 @@ public ObservationsSimple(ObservationsSimple obs, int permut[]) // Mutators + /** + * Initialise observation info for {@code numToAdd} new observations. + */ + public void addObservations(int numToAdd) + { + for (int i = 0; i < numToAdd; i++) { + observationsList.add(null); + observationStates.add(-1); + } + } + /** * Clear observation info for state {@code s}. */ @@ -212,7 +226,7 @@ public void setObservation(int s, State observ, State unobserv, List obs unobservIndex = unobservationsList.size() - 1; } // Assign the unobservation (index) to the state - unobservablesMap.set(s, unobservIndex); + setUnobservation(s, unobservIndex); } /** @@ -243,6 +257,17 @@ protected void setObservation(int s, int o, NondetModel model) throws PrismExcep } } + /** + * Assign unobservation with index u to state s. + * (assumes unobservation has already been added to the list) + * @param s State + * @param u Unobservation + */ + protected void setUnobservation(int s, int u) + { + unobservablesMap.set(s, u); + } + /** * Set the observation for each state {@code s} to be {@code s}. */ diff --git a/prism/src/explicit/POMDPSimple.java b/prism/src/explicit/POMDPSimple.java index adcab61a1e..9916873e85 100644 --- a/prism/src/explicit/POMDPSimple.java +++ b/prism/src/explicit/POMDPSimple.java @@ -33,6 +33,7 @@ import java.util.Map; import explicit.rewards.MDPRewards; +import io.ExplicitModelImporter; import parser.State; import prism.PrismException; import prism.PrismUtils; @@ -117,6 +118,17 @@ public void addStates(int numToAdd) observations.addStates(numToAdd); } + @Override + public void buildFromExplicitImport(ExplicitModelImporter modelImporter) throws PrismException + { + super.buildFromExplicitImport(modelImporter); + observations = new ObservationsSimple(modelImporter.getNumStates(), modelImporter.getNumObservations()); + modelImporter.extractObservations(this::setObservation); + for (int s = 0; s < numStates; s++) { + observations.setUnobservation(s, s); + } + } + // Mutators (other) /** diff --git a/prism/src/explicit/graphviz/ShowStatesDecorator.java b/prism/src/explicit/graphviz/ShowStatesDecorator.java index 10d8b48bb5..972c5be235 100644 --- a/prism/src/explicit/graphviz/ShowStatesDecorator.java +++ b/prism/src/explicit/graphviz/ShowStatesDecorator.java @@ -65,7 +65,9 @@ public ShowStatesDecorator(List stateList, Function obsLi /** Decorate state label by appending the variable information */ public Decoration decorateState(int state, Decoration d) { - d.labelAddBelow(stateList.get(state).toString()); + if (stateList != null) { + d.labelAddBelow(stateList.get(state).toString()); + } if (obsList != null) { State o = obsList.apply(state); if (o != null) { diff --git a/prism/src/io/DotExporter.java b/prism/src/io/DotExporter.java index 710575cb93..182738c102 100644 --- a/prism/src/io/DotExporter.java +++ b/prism/src/io/DotExporter.java @@ -83,12 +83,14 @@ public void exportModel(Model model, PrismLog out, Iterable) model)::getObservationAsState).decorateState(s, d); - } else { - d = new explicit.graphviz.ShowStatesDecorator(model.getStatesList()).decorateState(s, d); - } + boolean showStates = modelExportOptions.getShowStates() && model.getStatesList() != null; + boolean showObs = modelType.partiallyObservable() && modelExportOptions.getShowObservations(); + if (showStates && showObs) { + d = new explicit.graphviz.ShowStatesDecorator(model.getStatesList(), ((PartiallyObservableModel) model)::getObservationAsState).decorateState(s, d); + } else if (showStates) { + d = new explicit.graphviz.ShowStatesDecorator(model.getStatesList()).decorateState(s, d); + } else if (showObs) { + d = new explicit.graphviz.ShowStatesDecorator(null, ((PartiallyObservableModel) model)::getObservationAsState).decorateState(s, d); } if (decorators != null) { for (Decorator decorator : decorators) { diff --git a/prism/src/io/ExplicitModelImporter.java b/prism/src/io/ExplicitModelImporter.java index b4916f3830..6848dbceb1 100644 --- a/prism/src/io/ExplicitModelImporter.java +++ b/prism/src/io/ExplicitModelImporter.java @@ -39,6 +39,7 @@ import java.util.BitSet; import java.util.function.BiConsumer; import java.util.function.Consumer; +import java.util.function.IntConsumer; /** * Base class for importers from explicit model sources. @@ -95,6 +96,11 @@ public void setModel(explicit.Model modelLookup) */ public abstract boolean providesStates(); + /** + * Does this importer provide info about observation definitions? + */ + public abstract boolean providesObservations(); + /** * Does this importer provide info about labels? */ @@ -128,6 +134,11 @@ public void setModel(explicit.Model modelLookup) */ public abstract int getNumTransitions() throws PrismException; + /** + * Get the number of observations. + */ + public abstract int getNumObservations() throws PrismException; + /** * Get the indices of the states which are/were deadlocks. */ @@ -154,9 +165,9 @@ public String getModelTypeString() throws PrismException /** * Extract state definitions (variable values). - * Calls {@code storeStateDefn(s, i, o)} for each state s, variable (index) i and variable value o. + * Calls {@code storeStateDefn(s, i, v)} for each state s, variable (index) i and variable value v. * If {@link #providesStates()} returns false, this should report a single - * integer-valued variable range between 0 and {@link #getNumStates()} - 1. + * integer-valued variable ranging between 0 and {@link #getNumStates()} - 1. * @param storeStateDefn Function to be called for each variable value of each state */ public void extractStates(IOUtils.StateDefnConsumer storeStateDefn) throws PrismException @@ -168,6 +179,22 @@ public void extractStates(IOUtils.StateDefnConsumer storeStateDefn) throws Prism } } + /** + * Extract observation definitions (observable values). + * Calls {@code storeObservationDefn(o, i, v)} for each observation o, observable (index) i and observable value v. + * If {@link #providesObservations()} returns false, this should report a single + * integer-valued observable ranging between 0 and {@link #getNumObservations()} - 1. + * @param storeObservationDefn Function to be called for each variable value of each state + */ + public void extractObservationDefinitions(IOUtils.StateDefnConsumer storeObservationDefn) throws PrismException + { + // Default implementation - assume one integer observable + int numObs = getNumObservations(); + for (int o = 0; o < numObs; o++) { + storeObservationDefn.accept(o, 0, o); + } + } + /** * Compute the maximum number of choices (in a nondeterministic model). */ @@ -242,6 +269,13 @@ public void extractLabelsAndInitialStates(BiConsumer storeLabe */ public abstract void extractLabelsAndInitialStates(BiConsumer storeLabel, Consumer storeInit, Consumer storeDeadlock) throws PrismException; + /** + * Extract info about (deterministic, state-based) observations. + * Calls {@code storeObservation(s, o)} for each state s giving its observation o. + * @param storeObservation Function to be called for each state + */ + public abstract void extractObservations(IOUtils.StateIntConsumer storeObservation) throws PrismException; + /** * Extract the state rewards for a given reward structure index. * The transition probabilities/rates are assumed to be of type double. @@ -312,7 +346,7 @@ public void extractMDPTransitionRewards(int rewardIndex, IOUtils.TransitionRewar */ public abstract void extractMDPTransitionRewards(int rewardIndex, IOUtils.TransitionRewardConsumer storeReward, Evaluator eval) throws PrismException; - // Defaults for a single variable name when none is specified + // Defaults for a single variable when none is specified /** * Get the default name for the (single) variable when none is specified. @@ -340,4 +374,24 @@ public DeclarationType defaultVariableDeclarationType() throws PrismException { return new DeclarationInt(Expression.Int(0), Expression.Int(getNumStates() - 1)); } + + // Defaults for a single observable when none is specified + + /** + * Get the default name for the (single) observable when none is specified. + * By default, this is "o". + */ + public String defaultObservableName() + { + return "o"; + } + + /** + * Get the default type for the (single) observable when none is specified. + * By default, this is {@code int}. + */ + public Type defaultObservableType() + { + return TypeInt.getInstance(); + } } diff --git a/prism/src/io/IOUtils.java b/prism/src/io/IOUtils.java index 1a6ac6f28f..0e0b9664fc 100644 --- a/prism/src/io/IOUtils.java +++ b/prism/src/io/IOUtils.java @@ -34,12 +34,12 @@ public class IOUtils { /** - * Functional interface for a consumer accepting state variable values (s,i,o), - * i.e., state s, variable index i, value o. + * Functional interface for a consumer accepting state variable values (s,i,v), + * i.e., state s, variable index i, value v. */ @FunctionalInterface public interface StateDefnConsumer { - void accept(int s, int i, Object o) throws PrismException; + void accept(int s, int i, Object v) throws PrismException; } /** @@ -69,6 +69,15 @@ public interface LTSTransitionConsumer { void accept(int s, int i, int s2, Object a) throws PrismException; } + /** + * Functional interface for a consumer accepting integer state values (s,v), + * i.e., state s, value v. + */ + @FunctionalInterface + public interface StateIntConsumer { + void accept(int s, int v) throws PrismException; + } + /** * Functional interface for a consumer accepting state values (s,v), * i.e., state s, value v. diff --git a/prism/src/io/ModelExportOptions.java b/prism/src/io/ModelExportOptions.java index c8e82eedc5..bc83ed4b00 100644 --- a/prism/src/io/ModelExportOptions.java +++ b/prism/src/io/ModelExportOptions.java @@ -50,6 +50,11 @@ public class ModelExportOptions implements Cloneable */ private Optional showStates = Optional.empty(); + /** + * Whether to show full observation details + */ + private Optional showObservations = Optional.empty(); + /** * Whether to show actions */ @@ -119,6 +124,15 @@ public ModelExportOptions setShowStates(boolean showStates) return this; } + /** + * Set whether to show full observation details. + */ + public ModelExportOptions setShowObservations(boolean showObservations) + { + this.showObservations = Optional.of(showObservations); + return this; + } + /** * Set whether to show actions. */ @@ -160,6 +174,9 @@ public void apply(ModelExportOptions other) if (other.showStates.isPresent()) { setShowStates(other.getShowStates()); } + if (other.showObservations.isPresent()) { + setShowObservations(other.getShowObservations()); + } if (other.showActions.isPresent()) { setShowActions(other.getShowActions()); } @@ -208,6 +225,14 @@ public boolean getShowStates() return showStates.orElse(true); } + /** + * Whether to show full observation details. + */ + public boolean getShowObservations() + { + return showObservations.orElse(true); + } + /** * Whether to show actions. */ diff --git a/prism/src/io/ModelExportTask.java b/prism/src/io/ModelExportTask.java index efad3164ab..425d4cf4d7 100644 --- a/prism/src/io/ModelExportTask.java +++ b/prism/src/io/ModelExportTask.java @@ -244,7 +244,6 @@ public static ModelExportTask fromOptions(File file, ModelExportOptions exportOp break; case DOT: exportTask = new ModelExportTask(ModelExportEntity.MODEL, file); - exportTask.getExportOptions().setShowStates(true); break; case DRN: exportTask = new ModelExportTask(ModelExportEntity.MODEL, file); diff --git a/prism/src/io/PrismExplicitExporter.java b/prism/src/io/PrismExplicitExporter.java index 3e14e31d49..900ad9a471 100644 --- a/prism/src/io/PrismExplicitExporter.java +++ b/prism/src/io/PrismExplicitExporter.java @@ -77,6 +77,8 @@ public void exportTransitions(Model model, PrismLog out) throws // Get model info and exportOptions ModelType modelType = model.getModelType(); boolean showActions = modelExportOptions.getShowActions(); + // Currently, we only include initial state info here for POMDPs + boolean showInit = modelType.partiallyObservable(); // Output .tra file file header int numStates = model.getNumStates(); @@ -90,6 +92,24 @@ public void exportTransitions(Model model, PrismLog out) throws } out.print("\n"); + // Output initial states, if required + if (showInit) { + for (int s : model.getInitialStates()) { + out.print("-"); + if (modelType.nondeterministic()) { + out.print(" -"); + } + out.print(" " + s); + if (modelType.isProbabilistic()) { + out.print(" -"); + } + if (modelType.partiallyObservable()) { + out.print(" " + ((PartiallyObservableModel) model).getObservation(s)); + } + out.print("\n"); + } + } + // Output transitions in .tra format // Iterate through states for (int s = 0; s < numStates; s++) { diff --git a/prism/src/io/PrismExplicitImporter.java b/prism/src/io/PrismExplicitImporter.java index 619481aae8..15679a56a7 100644 --- a/prism/src/io/PrismExplicitImporter.java +++ b/prism/src/io/PrismExplicitImporter.java @@ -80,10 +80,13 @@ public class PrismExplicitImporter extends ExplicitModelImporter // What to import: files and type override private File statesFile; private File transFile; + private File observationsFile; private File labelsFile; private List stateRewardsFiles; private List transRewardsFiles; private ModelType typeOverride; + // Does the transitions file store initial states info? + private boolean transFileStoresInitialStates; // Model info extracted from files and then stored in a BasicModelInfo object private BasicModelInfo basicModelInfo; @@ -97,6 +100,7 @@ private class ModelStats int numStates = 0; int numChoices = 0; int numTransitions = 0; + int numObservations = 0; } private ModelStats modelStats; @@ -191,6 +195,15 @@ public void setTransFile(File transFile) this.transFile = transFile; } + /** + * Set the observations file. + * @param observationsFile Observations file (may be {@code null}) + */ + public void setObservationsFile(File observationsFile) + { + this.observationsFile = observationsFile; + } + /** * Set the labels file. * @param labelsFile Labels file (may be {@code null}) @@ -236,6 +249,14 @@ public File getTransFile() return transFile; } + /** + * Get the observations file (null if not used). + */ + public File getObservationsFile() + { + return observationsFile; + } + /** * Get the labels file (null if not used). */ @@ -256,6 +277,9 @@ public List getAllFiles() if (statesFile != null) { allFiles.add(statesFile); } + if (observationsFile != null) { + allFiles.add(observationsFile); + } if (labelsFile != null) { allFiles.add(labelsFile); } @@ -274,12 +298,29 @@ public boolean providesStates() return getStatesFile() != null; } + @Override + public boolean providesObservations() + { + return getObservationsFile() != null; + } + @Override public boolean providesLabels() { return getLabelsFile() != null; } + /** + * Does the transitions file store initial states info? + */ + private boolean transFileProvidesInitialStates() throws PrismException + { + if (modelStats == null) { + buildModelStats(); + } + return transFileStoresInitialStates; + } + @Override public String sourceString() { @@ -339,6 +380,20 @@ public int getNumTransitions() throws PrismException return numTransitions; } + @Override + public int getNumObservations() throws PrismException + { + // Construct lazily, as needed + // (determined from transitions file, if needed) + if (!getModelInfo().getModelType().partiallyObservable()) { + return 0; + } + if (modelStats == null) { + buildModelStats(); + } + return modelStats.numObservations; + } + @Override public BitSet getDeadlockStates() throws PrismException { @@ -426,6 +481,16 @@ private void buildModelInfo() throws PrismException basicModelInfo.getVarList().addVar(defaultVariableName(), defaultVariableDeclarationType(), -1); } + // Extract observable info from observations, if available + if (modelType.partiallyObservable() && observationsFile != null) { + extractObservableInfoFromObservationsFile(observationsFile); + } + // Otherwise store default observable info + else { + basicModelInfo.getObservableNames().add(defaultObservableName()); + basicModelInfo.getObservableTypeList().add(defaultObservableType()); + } + // Generate and store label names from the labels file, if available. // This way, expressions can refer to the labels later on. if (labelsFile != null) { @@ -440,18 +505,36 @@ private void buildModelInfo() throws PrismException */ private void extractVarInfoFromStatesFile(File statesFile) throws PrismException { - int i, j, lineNum = 0; + extractVarInfoFromFile(statesFile, ModelExportTask.ModelExportEntity.STATES); + } + /** + * Extract observable info from an observations file. + */ + private void extractObservableInfoFromObservationsFile(File observationsFile) throws PrismException + { + extractVarInfoFromFile(observationsFile, ModelExportTask.ModelExportEntity.OBSERVATIONS); + } + + /** + * Extract variable/observable info from a states/observations file. + * @param file States/observations file + * @param entity State or observations? + */ + private void extractVarInfoFromFile(File file, ModelExportTask.ModelExportEntity entity) throws PrismException + { + String entityString = (entity == ModelExportTask.ModelExportEntity.STATES) ? "state" : "observation"; // open file for reading, automatic close when done - try (BufferedReader in = new BufferedReader(new FileReader(statesFile))) { + int lineNum = 0; + try (BufferedReader in = new BufferedReader(new FileReader(file))) { // read first line and extract var names String s = in.readLine(); lineNum = 1; if (s == null) - throw new PrismException("empty states file"); + throw new PrismException("empty " + entityString + "s file"); s = s.trim(); if (s.charAt(0) != '(' || s.charAt(s.length() - 1) != ')') - throw new PrismException("badly formatted state"); + throw new PrismException("badly formatted " + entityString); s = s.substring(1, s.length() - 1); List varNames = new ArrayList<>(Arrays.asList(s.split(","))); int numVars = varNames.size(); @@ -474,8 +557,8 @@ private void extractVarInfoFromStatesFile(File statesFile) throws PrismException if (ss.length != numVars) throw new PrismException("wrong number of variables"); // for each variable... - for (i = 0; i < numVars; i++) { - // if this is the first state, establish variable type + for (int i = 0; i < numVars; i++) { + // if this is the first state/observation, establish variable type if (counter == 1) { if (ss[i].equals("true") || ss[i].equals("false")) { varTypes.add(TypeBool.getInstance()); @@ -485,7 +568,7 @@ private void extractVarInfoFromStatesFile(File statesFile) throws PrismException } // check for new min/max values (ints only) if (varTypes.get(i) instanceof TypeInt) { - j = Integer.parseInt(ss[i]); + int j = Integer.parseInt(ss[i]); if (counter == 1) { varMins[i] = varMaxs[i] = j; } else { @@ -502,25 +585,33 @@ private void extractVarInfoFromStatesFile(File statesFile) throws PrismException lineNum++; } - // Add variables to the VarList - for (i = 0; i < numVars; i++) { - if (varTypes.get(i) instanceof TypeBool) { - basicModelInfo.getVarList().addVar(varNames.get(i), new DeclarationBool(), -1); - } else { - // Note: we do not yet allow 0-range variables - if (varMins[i] == varMaxs[i]) { - varMaxs[i]++; + if (entity == ModelExportTask.ModelExportEntity.STATES) { + // Add variables to the VarList + for (int i = 0; i < numVars; i++) { + if (varTypes.get(i) instanceof TypeBool) { + basicModelInfo.getVarList().addVar(varNames.get(i), new DeclarationBool(), -1); + } else { + // Note: we do not yet allow 0-range variables + if (varMins[i] == varMaxs[i]) { + varMaxs[i]++; + } + basicModelInfo.getVarList().addVar(varNames.get(i), new DeclarationInt(Expression.Int(varMins[i]), Expression.Int(varMaxs[i])), -1); } - basicModelInfo.getVarList().addVar(varNames.get(i), new DeclarationInt(Expression.Int(varMins[i]), Expression.Int(varMaxs[i])), -1); + } + } else if (entity == ModelExportTask.ModelExportEntity.OBSERVATIONS) { + // Add observables to the model info + for (int i = 0; i < numVars; i++) { + basicModelInfo.getObservableNameList().add(varNames.get(i)); + basicModelInfo.getObservableTypeList().add(varTypes.get(i)); } } } catch (IOException e) { - throw new PrismException("File I/O error reading from \"" + statesFile + "\""); + throw new PrismException("File I/O error reading from \"" + file + "\""); } catch (NumberFormatException e) { - throw new PrismException("Error detected at line " + lineNum + " of states file \"" + statesFile + "\""); + throw new PrismException("Error detected at line " + lineNum + " of " + entityString + "s file \"" + file + "\""); } catch (PrismException e) { - throw new PrismException("Error detected (" + e.getMessage() + ") at line " + lineNum + " of states file \"" + statesFile + "\""); + throw new PrismException("Error detected (" + e.getMessage() + ") at line " + lineNum + " of " + entityString + "s file \"" + file + "\""); } } @@ -537,24 +628,39 @@ private void extractModelStatsFromTransFile(File transFile) throws PrismExceptio throw new PrismException("empty transitions file"); } String[] record = csv.nextRecord(); - checkLineSize(record, 2, 3); + checkLineSize(record, 2, 4); modelStats.numStates = Integer.parseInt(record[0]); if (record.length == 2) { + // Markov chain modelStats.numChoices = modelStats.numStates; modelStats.numTransitions = Integer.parseInt(record[1]); + } else if (record.length == 3) { + // MDP/LTS + modelStats.numChoices = Integer.parseInt(record[1]); + modelStats.numTransitions = Integer.parseInt(record[2]); } else { + // POMDP modelStats.numChoices = Integer.parseInt(record[1]); modelStats.numTransitions = Integer.parseInt(record[2]); + modelStats.numObservations = Integer.parseInt(record[3]); + } + // Also peek at the next line to see if initial states info is provided + if (csv.hasNextRecord()) { + record = csv.nextRecord(); + if (record.length >= 1 && record[0].equals("-")) { + transFileStoresInitialStates = true; + } } } catch (IOException e) { modelStats = null; throw new PrismException("File I/O error reading from \"" + transFile + "\""); - } catch (NumberFormatException | CsvFormatException e) { + } catch (PrismException | NumberFormatException | CsvFormatException e) { modelStats = null; - throw new PrismException("Error detected at line 1 of transitions file \"" + transFile + "\""); + int lineNum = 1; + String expl = (e.getMessage() == null || e.getMessage().isEmpty()) ? "" : (" (" + e.getMessage() + ")"); + throw new PrismException("Error detected" + expl + " at line " + lineNum + " of transitions file \"" + transFile + "\""); } } - /** * Extract names of labels from the labels file. @@ -617,6 +723,7 @@ private ModelType autodetectModelType(File transFile) BasicReader reader = BasicReader.wrap(in).normalizeLineEndings(); CsvReader csv = new CsvReader(reader, false, false, false, ' ', LF); boolean nondet; + boolean partObs; boolean nonprob; // Examine first line // 3 numbers should indicate a nondeterministic model, e.g., MDP @@ -627,10 +734,15 @@ private ModelType autodetectModelType(File transFile) } // Detect if model is nondeterministic String[] recordFirst = csv.nextRecord(); - if (recordFirst.length == 3) { + if (recordFirst.length == 4) { + nondet = true; + partObs = true; + } else if (recordFirst.length == 3) { nondet = true; + partObs = false; } else if (recordFirst.length == 2) { nondet = false; + partObs = false; } else { return null; } @@ -641,7 +753,8 @@ private ModelType autodetectModelType(File transFile) if (lines > max) { break; } - if ("".equals(record[0])) { + // Skip blank lines or initial states lines + if ("".equals(record[0]) || "-".equals(record[0])) { continue; } lines++; @@ -685,8 +798,8 @@ private ModelType autodetectModelType(File transFile) return ModelType.CTMC; } } - // All non-rates seen: guess MDP/DTMC - return nondet ? ModelType.MDP : ModelType.DTMC; + // All non-rates seen: guess (PO)MDP/DTMC + return nondet ? (partObs ? ModelType.POMDP : ModelType.MDP) : ModelType.DTMC; } catch (NumberFormatException | CsvFormatException | IOException e) { return null; } @@ -707,12 +820,12 @@ private void findDeadlocks() throws PrismException CsvReader csv = new CsvReader(reader, false, false, false, ' ', LF); for (String[] record : csv) { lineNum++; - if ("".equals(record[0])) { - // Skip blank lines + // Skip blank lines or initial states lines + if ("".equals(record[0]) || "-".equals(record[0])) { continue; } - // Lines should be 3-5 long (LTS/MDP with/without actions) - checkLineSize(record, 3, 5); + // Lines should be 3-6 long (LTS/MDP/POMDP with/without actions) + checkLineSize(record, 3, 6); // Extract/store source state int s = checkStateIndex(Integer.parseInt(record[0]), modelStats.numStates); statesWithTransitions.set(s); @@ -742,9 +855,32 @@ public void extractStates(IOUtils.StateDefnConsumer storeStateDefn) throws Prism return; } // Otherwise extract from .sta file - int numVars = basicModelInfo.getNumVars(); + extractStateDefinitions(statesFile, basicModelInfo.getNumVars(), storeStateDefn); + } + + @Override + public void extractObservationDefinitions(IOUtils.StateDefnConsumer storeObservationDefn) throws PrismException + { + // If there is no info, just assume that observations comprise a single integer observable + if (getObservationsFile() == null) { + super.extractObservationDefinitions(storeObservationDefn); + return; + } + // Otherwise extract from .obs file + extractStateDefinitions(observationsFile, basicModelInfo.getNumObservables(), storeObservationDefn); + } + + /** + * Extract state definitions from a states/observables (.sta/.obs) file. + * Calls {@code storeStateDefn(s, i, v)} for each state s, variable (index) i and variable value v. + * @param file States/observations (.sta/.obs) file + * @param numVars Number of variables/observables + * @param storeStateDefn Consumer to store state/observation definitions + */ + private void extractStateDefinitions(File file, int numVars, IOUtils.StateDefnConsumer storeStateDefn) throws PrismException + { int lineNum = 0; - try (BufferedReader in = new BufferedReader(new FileReader(statesFile))) { + try (BufferedReader in = new BufferedReader(new FileReader(file))) { lineNum += skipCommentAndFirstLine(in); String st = in.readLine(); lineNum++; @@ -775,10 +911,10 @@ public void extractStates(IOUtils.StateDefnConsumer storeStateDefn) throws Prism lineNum++; } } catch (IOException e) { - throw new PrismException("File I/O error reading from \"" + statesFile + "\""); + throw new PrismException("File I/O error reading from \"" + file + "\""); } catch (PrismException | NumberFormatException e) { String expl = (e.getMessage() == null || e.getMessage().isEmpty()) ? "" : (" (" + e.getMessage() + ")"); - throw new PrismException("Error detected" + expl + " at line " + lineNum + " of states file \"" + statesFile + "\""); + throw new PrismException("Error detected" + expl + " at line " + lineNum + " of states file \"" + file + "\""); } } @@ -793,12 +929,12 @@ public int computeMaxNumChoices() throws PrismException CsvReader csv = new CsvReader(reader, false, false, false, ' ', LF); for (String[] record : csv) { lineNum++; - if ("".equals(record[0])) { - // Skip blank lines + // Skip blank lines or initial states lines + if ("".equals(record[0]) || "-".equals(record[0])) { continue; } - // Lines should be 3-5 long (LTS/MDP with/without actions) - checkLineSize(record, 3, 5); + // Lines should be 3-5 long (LTS/MDP/POMDP with/without actions) + checkLineSize(record, 3, 6); int j = checkChoiceIndex(Integer.parseInt(record[1])); if (j + 1 > maxNumChoices) { maxNumChoices = j + 1; @@ -832,8 +968,8 @@ public void extractMCTransitions(IOUtils.MCTransitionConsumer sto CsvReader csv = new CsvReader(reader, false, false, false, ' ', LF); for (String[] record : csv) { lineNum++; - if ("".equals(record[0])) { - // Skip blank lines + // Skip blank lines or initial states lines + if ("".equals(record[0]) || "-".equals(record[0])) { continue; } checkLineSize(record, 3, 4); @@ -878,16 +1014,18 @@ public void extractMDPTransitions(IOUtils.MDPTransitionConsumer s CsvReader csv = new CsvReader(reader, false, false, false, ' ', LF); for (String[] record : csv) { lineNum++; - if ("".equals(record[0])) { - // Skip blank lines + // Skip blank lines or initial states lines + if ("".equals(record[0]) || "-".equals(record[0])) { continue; } - checkLineSize(record, 4, 5); + // Lines should be 4-6 long (MDP/POMDP with/without actions) + checkLineSize(record, 4, 6); int s = checkStateIndex(Integer.parseInt(record[0]), modelStats.numStates); int i = checkChoiceIndex(Integer.parseInt(record[1])); int s2 = checkStateIndex(Integer.parseInt(record[2]), modelStats.numStates); Value v = checkValue(record[3], eval); - Object a = (record.length > 4) ? checkAction(record[4]) : null; + int actIndex = getModelInfo().getModelType().partiallyObservable() ? 5 : 4; + Object a = (record.length > actIndex) ? checkAction(record[actIndex]) : null; // Add self-loops for any deadlock states before s while (nextDeadlock != -1 && nextDeadlock < s) { storeTransition.accept(nextDeadlock, 0, nextDeadlock, eval.one(), null); @@ -925,8 +1063,8 @@ public void extractLTSTransitions(IOUtils.LTSTransitionConsumer storeTransition) CsvReader csv = new CsvReader(reader, false, false, false, ' ', LF); for (String[] record : csv) { lineNum++; - if ("".equals(record[0])) { - // Skip blank lines + // Skip blank lines or initial states lines + if ("".equals(record[0]) || "-".equals(record[0])) { continue; } checkLineSize(record, 3, 4); @@ -958,12 +1096,27 @@ public void extractLTSTransitions(IOUtils.LTSTransitionConsumer storeTransition) @Override public void extractLabelsAndInitialStates(BiConsumer storeLabel, Consumer storeInit, Consumer storeDeadlock) throws PrismException { - // If there is no info, just assume that 0 is the initial state + // Extract any initial states info from the .tra file first + BitSet initialStatesTra = new BitSet(); + if (transFileProvidesInitialStates()) { + extractInitialStatesFromTransFile(initialStatesTra::set); + } + + // If there is no .lab file, we are done; just store initial states + // Assume that 0 is the initial state in the absence of any other info if (getLabelsFile() == null) { - storeInit.accept(0); + if (transFileProvidesInitialStates()) { + for (int s = initialStatesTra.nextSetBit(0); s >= 0; s = initialStatesTra.nextSetBit(s + 1)) { + storeInit.accept(s); + } + } else { + storeInit.accept(0); + } return; } + // Otherwise extract from .lab file + BitSet initialStatesLab = new BitSet(); int lineNum = 0; try (BufferedReader in = new BufferedReader(new FileReader(labelsFile))) { // Skip first file (label names extracted earlier with model info) @@ -989,7 +1142,7 @@ public void extractLabelsAndInitialStates(BiConsumer storeLabe storeDeadlock.accept(s); } } else if (l == -1) { - storeInit.accept(s); + initialStatesLab.set(i); } else if (l > -1) { storeLabel.accept(s, l); } @@ -998,6 +1151,18 @@ public void extractLabelsAndInitialStates(BiConsumer storeLabe // Prepare for next iter st = in.readLine(); } + + // If initial states were provided in .tra file, we check for consistency with .lab file + if (transFileProvidesInitialStates()) { + if (!initialStatesTra.equals(initialStatesLab)) { + throw new PrismException("Inconsistent initial states information between transitions and labels files"); + } + } + + // Finally, store initial states + for (int s = initialStatesLab.nextSetBit(0); s >= 0; s = initialStatesLab.nextSetBit(s + 1)) { + storeInit.accept(s); + } } catch (IOException e) { throw new PrismException("File I/O error reading from \"" + labelsFile + "\""); } catch (PrismException | NumberFormatException e) { @@ -1006,6 +1171,91 @@ public void extractLabelsAndInitialStates(BiConsumer storeLabe } } + @Override + public void extractObservations(IOUtils.StateIntConsumer storeObservation) throws PrismException + { + // Skip this if model is not partially observable + if (!getModelInfo().getModelType().partiallyObservable()) { + return; + } + + // Extract observations from transitions file + // Temporarily store in an array to check for conflicting info + int observations[] = new int[modelStats.numStates]; + Arrays.fill(observations, -1); + int lineNum = 0; + try (BufferedReader in = new BufferedReader(new FileReader(transFile))) { + lineNum += skipCommentAndFirstLine(in); + BasicReader reader = BasicReader.wrap(in).normalizeLineEndings(); + CsvReader csv = new CsvReader(reader, false, false, false, ' ', LF); + for (String[] record : csv) { + lineNum++; + if ("".equals(record[0])) { + // Skip blank lines + continue; + } + // Lines should be 5-6 long (POMDP with/without actions) + checkLineSize(record, 5, 6); + int s2 = checkStateIndex(Integer.parseInt(record[2]), modelStats.numStates); + int o = checkStateIndex(Integer.parseInt(record[4]), modelStats.numStates); + // Check/store observation + if (observations[s2] != -1 && observations[s2] != o) { + throw new PrismException("Conflicting observation information for state " + s2); + } + observations[s2] = o; + } + // Finally, store observations in the model + for (int s = 0; s < modelStats.numStates; s++) { + if (observations[s] == -1) { + throw new PrismException("No observation information for state " + s); + } else { + storeObservation.accept(s, observations[s]); + } + } + } catch (IOException e) { + throw new PrismException("File I/O error reading from \"" + transFile + "\""); + } catch (PrismException | NumberFormatException | CsvFormatException e) { + String expl = (e.getMessage() == null || e.getMessage().isEmpty()) ? "" : (" (" + e.getMessage() + ")"); + throw new PrismException("Error detected" + expl + " at line " + lineNum + " of transitions file \"" + transFile + "\""); + } + } + + /** + * Extract any info about initial states stored in the .tra file. + * Calls {@code storeInit(s)} for each initial state s. + * @param storeInit Function to be called for each initial state + */ + private void extractInitialStatesFromTransFile(Consumer storeInit) throws PrismException + { + ModelType modelType = getModelInfo().getModelType(); + int stateField = modelType.nondeterministic() ? 2 : 1; + int lineNum = 0; + try (BufferedReader in = new BufferedReader(new FileReader(transFile))) { + lineNum += skipCommentAndFirstLine(in); + BasicReader reader = BasicReader.wrap(in).normalizeLineEndings(); + CsvReader csv = new CsvReader(reader, false, false, false, ' ', LF); + for (String[] record : csv) { + lineNum++; + // Skip blank lines + if ("".equals(record[0])) { + continue; + } + checkLineSize(record, 3, 6); + // Break as soon as a non-initial states line is found + if (!"-".equals(record[0])) { + break; + } + int s2 = checkStateIndex(Integer.parseInt(record[stateField]), modelStats.numStates); + storeInit.accept(s2); + } + } catch (IOException e) { + throw new PrismException("File I/O error reading from \"" + transFile + "\""); + } catch (PrismException | NumberFormatException | CsvFormatException e) { + String expl = (e.getMessage() == null || e.getMessage().isEmpty()) ? "" : (" (" + e.getMessage() + ")"); + throw new PrismException("Error detected" + expl + " at line " + lineNum + " of transitions file \"" + transFile + "\""); + } + } + /** * Load all labels from a PRISM labels (.lab) file and store them in BitSet objects. * Return a map from label name Strings to BitSets. diff --git a/prism/src/prism/BasicModelInfo.java b/prism/src/prism/BasicModelInfo.java index 57974bf62f..334206988b 100644 --- a/prism/src/prism/BasicModelInfo.java +++ b/prism/src/prism/BasicModelInfo.java @@ -48,6 +48,10 @@ public class BasicModelInfo implements ModelInfo private List actionList; /** Variable list */ private VarList varList; + /** Observable name list */ + private List observableNameList; + /** Observable type list */ + private List observableTypeList; /** Label names */ private List labelNameList; @@ -61,6 +65,8 @@ public BasicModelInfo(ModelType modelType) this.modelType = modelType; actionList = null; varList = new VarList(); + observableNameList = new ArrayList<>(); + observableTypeList = new ArrayList<>(); labelNameList = new ArrayList<>(); } @@ -90,6 +96,22 @@ public void setVarList(VarList varList) this.varList = varList; } + /** + * Set the list used to store observable names. + */ + public void setObservableNameList(List observableNameList) + { + this.observableNameList = observableNameList; + } + + /** + * Set the list used to store observable types. + */ + public void setObservableTypeList(List observableTypeList) + { + this.observableTypeList = observableTypeList; + } + /** * Set the list used to store label names. */ @@ -114,6 +136,22 @@ public VarList getVarList() return varList; } + /** + * Get the list used to store observable names. + */ + public List getObservableNameList() + { + return observableNameList; + } + + /** + * Get the list used to store observable types. + */ + public List getObservableTypeList() + { + return observableTypeList; + } + /** * Get the list used to store label names. */ @@ -158,6 +196,18 @@ public DeclarationType getVarDeclarationType(int i) return varList.getDeclarationType(i); } + @Override + public List getObservableNames() + { + return observableNameList; + } + + @Override + public List getObservableTypes() + { + return observableTypeList; + } + @Override public List getLabelNames() { diff --git a/prism/src/prism/Prism.java b/prism/src/prism/Prism.java index 8d950dbaf0..db520eeeb3 100644 --- a/prism/src/prism/Prism.java +++ b/prism/src/prism/Prism.java @@ -4656,10 +4656,12 @@ public static ModelExportOptions convertExportType(int exportType) case Prism.EXPORT_DOT: exportOptions.setFormat(ModelExportFormat.DOT); exportOptions.setShowStates(false); + exportOptions.setShowObservations(false); break; case Prism.EXPORT_DOT_STATES: exportOptions.setFormat(ModelExportFormat.DOT); exportOptions.setShowStates(true); + exportOptions.setShowObservations(true); break; case Prism.EXPORT_ROWS: exportOptions.setFormat(ModelExportFormat.EXPLICIT); diff --git a/prism/src/prism/PrismCL.java b/prism/src/prism/PrismCL.java index 8655bdef7a..03d14c5a2e 100644 --- a/prism/src/prism/PrismCL.java +++ b/prism/src/prism/PrismCL.java @@ -742,6 +742,12 @@ private void sortModelImports() throws PrismException } importer.setStatesFile(modelImportSource.file); break; + case OBSERVATIONS: + if (importer.getObservationsFile() != null) { + throw new PrismException("Multiple observation files provided for model import"); + } + importer.setObservationsFile(modelImportSource.file); + break; case LABELS: if (importer.getLabelsFile() != null) { throw new PrismException("Multiple label files provided for model import"); @@ -843,7 +849,7 @@ private void doExports() throws PrismException try { File dotFile = File.createTempFile("prism-dot-", ".dot", null); File dotPdfFile = File.createTempFile("prism-dot-", ".dot.pdf", null); - prism.exportBuiltModelTransitions(dotFile, new ModelExportOptions().setFormat(ModelExportFormat.DOT).setShowStates(true)); + prism.exportBuiltModelTransitions(dotFile, new ModelExportOptions().setFormat(ModelExportFormat.DOT).setShowStates(true).setShowObservations(true)); (new ProcessBuilder(new String[]{ "dot", "-Tpdf", "-o", dotPdfFile.getPath(), dotFile.getPath()})).start().waitFor(); (new ProcessBuilder(new String[]{ "open",dotPdfFile.getPath()})).start(); } @@ -1273,6 +1279,14 @@ else if (sw.equals("importstates")) { errorAndExit("No file specified for -" + sw + " switch"); } } + // import observations for explicit model import + else if (sw.equals("importobs")) { + if (i < args.length - 1) { + modelImportSources.add(new ModelImportSource(ModelExportTask.ModelExportEntity.OBSERVATIONS, ModelExportFormat.EXPLICIT, new File(args[++i]))); + } else { + errorAndExit("No file specified for -" + sw + " switch"); + } + } // import labels for explicit model import else if (sw.equals("importlabels")) { if (i < args.length - 1) { @@ -1501,7 +1515,7 @@ else if (sw.equals("exportunordered") || sw.equals("unordered")) { // export transition matrix graph to dot file else if (sw.equals("exporttransdot")) { if (i < args.length - 1) { - ModelExportOptions exportOptions = new ModelExportOptions().setFormat(ModelExportFormat.DOT).setShowStates(false); + ModelExportOptions exportOptions = new ModelExportOptions().setFormat(ModelExportFormat.DOT).setShowStates(false).setShowObservations(false); modelExportTasks.add(new ModelExportTask(ModelExportTask.ModelExportEntity.MODEL, args[++i], exportOptions)); } else { errorAndExit("No file specified for -" + sw + " switch"); @@ -1510,7 +1524,7 @@ else if (sw.equals("exporttransdot")) { // export transition matrix graph to dot file (with states) else if (sw.equals("exporttransdotstates")) { if (i < args.length - 1) { - ModelExportOptions exportOptions = new ModelExportOptions().setFormat(ModelExportFormat.DOT).setShowStates(true); + ModelExportOptions exportOptions = new ModelExportOptions().setFormat(ModelExportFormat.DOT).setShowStates(true).setShowObservations(true); modelExportTasks.add(new ModelExportTask(ModelExportTask.ModelExportEntity.MODEL, args[++i], exportOptions)); } else { errorAndExit("No file specified for -" + sw + " switch"); @@ -1896,18 +1910,21 @@ private void processImportModelSwitch(String filesOptionsString) throws PrismExc // Items to import if (ext.equals("all")) { modelFilename = basename + ".tra"; - modelImportSources.add(new ModelImportSource(ModelExportTask.ModelExportEntity.MODEL, ModelExportFormat.EXPLICIT, new File(basename + ".tra"))); - modelImportSources.add(new ModelImportSource(ModelExportTask.ModelExportEntity.STATES, ModelExportFormat.EXPLICIT, new File(basename + ".sta"))); - modelImportSources.add(new ModelImportSource(ModelExportTask.ModelExportEntity.LABELS, ModelExportFormat.EXPLICIT, new File(basename + ".lab"))); + addModelImport(ModelExportTask.ModelExportEntity.MODEL,basename + ".tra", false); + addModelImport(ModelExportTask.ModelExportEntity.STATES,basename + ".sta", false); + addModelImport(ModelExportTask.ModelExportEntity.OBSERVATIONS,basename + ".obs", false); + addModelImport(ModelExportTask.ModelExportEntity.LABELS,basename + ".lab", false); addStateRewardImports(basename, false); addTransitionRewardImports(basename, false); } else if (ext.equals("tra")) { modelFilename = basename + ".tra"; - modelImportSources.add(new ModelImportSource(ModelExportTask.ModelExportEntity.MODEL, ModelExportFormat.EXPLICIT, new File(basename + ".tra"))); + addModelImport(ModelExportTask.ModelExportEntity.MODEL,basename + ".tra", true); } else if (ext.equals("sta")) { - modelImportSources.add(new ModelImportSource(ModelExportTask.ModelExportEntity.STATES, ModelExportFormat.EXPLICIT, new File(basename + ".sta"))); + addModelImport(ModelExportTask.ModelExportEntity.STATES,basename + ".sta", true); + } else if (ext.equals("obs")) { + addModelImport(ModelExportTask.ModelExportEntity.OBSERVATIONS,basename + ".obs", true); } else if (ext.equals("lab")) { - modelImportSources.add(new ModelImportSource(ModelExportTask.ModelExportEntity.LABELS, ModelExportFormat.EXPLICIT, new File(basename + ".lab"))); + addModelImport(ModelExportTask.ModelExportEntity.LABELS,basename + ".lab", true); } else if (ext.equals("srew")) { addStateRewardImports(basename, true); } else if (ext.equals("trew")) { @@ -1916,7 +1933,7 @@ private void processImportModelSwitch(String filesOptionsString) throws PrismExc // For any other extension (including none/unknown), default to explicit (.tra) else { modelFilename = basename + (ext.isEmpty() ? "" : "." + ext); - modelImportSources.add(new ModelImportSource(ModelExportTask.ModelExportEntity.MODEL, ModelExportFormat.EXPLICIT, new File(modelFilename))); + addModelImport(ModelExportTask.ModelExportEntity.MODEL,modelFilename, true); } } // No options supported currently @@ -1932,7 +1949,20 @@ private void processImportModelSwitch(String filesOptionsString) throws PrismExc } }*/ } - + + /** + * Add a model import file to {@code modelImportSources}. + * @param entity Model entity + * @param filename Model import filename + * @param assumeExists If true, we add the file even if it does not exist + */ + private void addModelImport(ModelExportTask.ModelExportEntity entity, String filename, boolean assumeExists) + { + if (assumeExists || new File(filename).exists()) { + modelImportSources.add(new ModelImportSource(entity, ModelExportFormat.EXPLICIT, new File(filename))); + } + } + /** * Given a file basename, find corresponding .srew files * and add them to {@code modelImportSources}. @@ -2133,6 +2163,28 @@ else if (opt.equals("proplabels")) { } } } + else if (opt.startsWith(sOpt = "states")) { + if (!opt.startsWith(sOpt + "=")) + throw new PrismException("No value provided for \"" + sOpt + "\" option of -exportmodel"); + String optVal = opt.substring(sOpt.length() + 1); + if (optVal.equals("true")) + exportOptions.setShowStates(true); + else if (optVal.equals("false")) + exportOptions.setShowStates(false); + else + throw new PrismException("Unknown value \"" + optVal + "\" provided for \"reach\" option of -exportstrat"); + } + else if (opt.startsWith(sOpt = "obs")) { + if (!opt.startsWith(sOpt + "=")) + throw new PrismException("No value provided for \"" + sOpt + "\" option of -exportmodel"); + String optVal = opt.substring(sOpt.length() + 1); + if (optVal.equals("true")) + exportOptions.setShowObservations(true); + else if (optVal.equals("false")) + exportOptions.setShowObservations(false); + else + throw new PrismException("Unknown value \"" + optVal + "\" provided for \"reach\" option of -exportstrat"); + } else if (opt.startsWith(sOpt = "actions")) { if (!opt.startsWith(sOpt + "=")) throw new PrismException("No value provided for \"" + sOpt + "\" option of -exportmodel"); @@ -2589,6 +2641,7 @@ private void printHelp() mainLog.println("-importmodel ........... Import the model directly from text file(s)"); mainLog.println("-importtrans ............ Import the transition matrix directly from a text file"); mainLog.println("-importstates ............ Import the list of states directly from a text file"); + mainLog.println("-importobs ............... Import the list of observations directly from a text file"); mainLog.println("-importlabels ............ Import the list of labels directly from a text file"); mainLog.println("-importstaterewards ...... Import the state rewards directly from a text file"); mainLog.println("-importtransrewards ...... Import the transition rewards directly from a text file"); @@ -2678,7 +2731,7 @@ else if (sw.equals("importmodel")) { mainLog.println("Import the model directly from text file(s)."); mainLog.println("Use a list of file extensions to indicate which files should be read, e.g.:"); mainLog.println("\n -importmodel in.tra,sta\n"); - mainLog.println("Possible extensions are: .tra, .sta, .lab, .srew, .trew"); + mainLog.println("Possible extensions are: .tra, .sta, .obs, .lab, .srew, .trew"); mainLog.println("Use extension .all to import all, e.g.:"); mainLog.println("\n -importmodel in.all\n"); } @@ -2731,6 +2784,8 @@ else if (sw.equals("exportmodel")) { mainLog.println(" * matlab - same as format=matlab"); mainLog.println(" * rows - export matrices with one row/distribution on each line"); mainLog.println(" * proplabels - export labels from a properties file into the same file, too"); + mainLog.println(" * states (=true/false) - include state definitions"); + mainLog.println(" * obs (=true/false) - include observation definitions"); mainLog.println(" * actions (=true/false) - show actions on choices/transitions"); mainLog.println(" * headers (=true/false) - include headers when exporting rewards"); mainLog.println(" * precision (=n) - export probabilities/rewards with n significant decimal places");