-exportstrat can export full induced model, including states/labels/rewards.

For example:

 prism ... -exportstrat strat.pexp
 prism ... -exportstrat strat.umb

The -exportstrat switch also gains many of -exportmodel's options:
format, states, rewards, labels, actions, precision, zip, text, headers.

To avoid an option clash, "obs" now means "show observations", like for
-exportmodel, and the existing "obs" option for -exportstrat is now
renamed to "mergeobs" (merge observationally equivalent states).

We also make reach=true the default.

Implementation details:

* StrategyExportOptions gains an inducedModelExportOptions field.

* Tidy up constructInducedModel and exportInducedModel in Strategy classes for
  explicit models to respect inducedModelExportOptions and to use new
  Model.export method, allow full model export to .pexp/.umb.

* Induced model construction in both ConstructInducedModel and
  ConstructStrategyProduct copies/lifts (by default, but optionally) any
  labels and rewards attached to the original model.

* Rewards are pre-emptively built and attached to built models when it is
  known that strategies are generated (via StateModelChecker.attachRewards)

Author: davexparker

prism-tests/functionality/export/strat/exportstratinduced.nm

@@ -0,0 +1,28 @@
+// Test for extended -exportstrat induced-model export: separate files (.tra/.sta/.lab),
+// combined formats (.pexp), mode=restrict/reduce and reach=true/false, all mirroring
+// -exportmodel's file/format/label handling. State 3 is reachable in the full model but
+// not under the optimal (Pmax) strategy for reaching "goal1", so it exercises reach=true
+// dropping/reindexing of unreachable states (and their labels).
+
+mdp
+
+module M
+
+s:[0..5];
+
+[east] s=0 -> 0.6:(s'=1) + 0.4:(s'=0);
+[south] s=0 -> 0.8:(s'=3) + 0.1:(s'=1) + 0.1:(s'=4);
+[east] s=1 -> 1:(s'=2);
+[south] s=1 -> 0.5:(s'=4) + 0.5:(s'=2);
+[stuck] s=2 -> 1:(s'=2);
+[stuck] s=3 -> 1:(s'=3);
+[east] s=4 -> 1:(s'=5);
+[west] s=4 -> 0.6:(s'=3) + 0.4:(s'=4);
+[north] s=5 -> 0.9:(s'=2) + 0.1:(s'=5);
+[west] s=5 -> 1:(s'=4);
+
+endmodule
+
+label "hazard" = s=1;
+label "goal1" = s=5;
+label "goal2" = s=2|s=3;

prism-tests/functionality/export/strat/exportstratinduced.nm.props

@@ -0,0 +1,2 @@
+// RESULT: 0.5
+Pmax=? [ F "goal1" ];

prism-tests/functionality/export/strat/exportstratinduced.nm.props.args

@@ -0,0 +1,4 @@
+-ex -exportstrat exportstratinduced.nm.props.tra
+-ex -exportstrat exportstratinduced.nm.props.reduce.pexp:type=induced,mode=reduce
+-ex -exportstrat exportstratinduced.nm.props.restrict.pexp:type=induced,mode=restrict
+-ex -exportstrat exportstratinduced.nm.props.reach.tra:type=induced,reach=true

prism-tests/functionality/export/strat/exportstratinduced.nm.props.multi.lab

@@ -0,0 +1,7 @@
+# Labels
+0="init" 1="deadlock" 2="hazard" 3="goal1" 4="goal2"
+0: 0
+1: 2
+2: 4
+3: 4
+5: 3

prism-tests/functionality/export/strat/exportstratinduced.nm.props.multi.sta

@@ -0,0 +1,8 @@
+# States
+(s)
+0:(0)
+1:(1)
+2:(2)
+3:(3)
+4:(4)
+5:(5)

prism-tests/functionality/export/strat/exportstratinduced.nm.props.multi.tra

@@ -0,0 +1,10 @@
+# Transitions (DTMC)
+6 8
+0 0 0.4 east
+0 1 0.6 east
+1 2 0.5 south
+1 4 0.5 south
+2 2 1 stuck
+3 3 1 stuck
+4 5 1 east
+5 4 1 west

prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.lab

@@ -0,0 +1,6 @@
+# Labels
+0="init" 1="deadlock" 2="hazard" 3="goal1" 4="goal2"
+0: 0
+1: 2
+2: 4
+4: 3

prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.sta

@@ -0,0 +1,7 @@
+# States
+(s)
+0:(0)
+1:(1)
+2:(2)
+3:(4)
+4:(5)

prism-tests/functionality/export/strat/exportstratinduced.nm.props.reach.tra

@@ -0,0 +1,9 @@
+# Transitions (DTMC)
+5 7
+0 0 0.4 east
+0 1 0.6 east
+1 2 0.5 south
+1 3 0.5 south
+2 2 1 stuck
+3 4 1 east
+4 3 1 west

prism-tests/functionality/export/strat/exportstratinduced.nm.props.reduce.pexp

@@ -0,0 +1,24 @@
+# Transitions (DTMC)
+5 7
+0 0 0.4 east
+0 1 0.6 east
+1 2 0.5 south
+1 3 0.5 south
+2 2 1 stuck
+3 4 1 east
+4 3 1 west
+
+# States
+(s)
+0:(0)
+1:(1)
+2:(2)
+3:(4)
+4:(5)
+
+# Labels
+0="init" 1="deadlock" 2="hazard" 3="goal1" 4="goal2"
+0: 0
+1: 2
+2: 4
+4: 3