diff --git a/prism-tests/functionality/import/dice2.lab b/prism-tests/functionality/import/dice2.lab new file mode 100644 index 00000000..a2a26ec7 --- /dev/null +++ b/prism-tests/functionality/import/dice2.lab @@ -0,0 +1,8 @@ +0="init" 1="deadlock" 2="end" 3="six" +0: 0 +7: 2 +8: 2 +9: 2 +10: 2 +11: 2 +12: 2 3 diff --git a/prism-tests/functionality/import/dice2.pm.importexport.auto b/prism-tests/functionality/import/dice2.pm.importexport.auto new file mode 100644 index 00000000..f3533db7 --- /dev/null +++ b/prism-tests/functionality/import/dice2.pm.importexport.auto @@ -0,0 +1,3 @@ +-dtmc -importmodel dice2.tra,lab,srew -exportmodel dice2.sta,tra,lab,srew +-dtmc -importmodel dice2.tra,lab,srew -exportmodel dice2.sta,tra,lab,srew -ex +-importmodel dice2.tra,lab,srew -exportmodel dice2.sta,tra,lab,srew -ex diff --git a/prism-tests/functionality/import/dice2.srew b/prism-tests/functionality/import/dice2.srew new file mode 100644 index 00000000..ffeb166e --- /dev/null +++ b/prism-tests/functionality/import/dice2.srew @@ -0,0 +1,8 @@ +13 7 +0 1 +1 1 +2 1 +3 1 +4 1 +5 1 +6 1 diff --git a/prism-tests/functionality/import/dice2.sta b/prism-tests/functionality/import/dice2.sta new file mode 100644 index 00000000..c85bc711 --- /dev/null +++ b/prism-tests/functionality/import/dice2.sta @@ -0,0 +1,14 @@ +(x) +0:(0) +1:(1) +2:(2) +3:(3) +4:(4) +5:(5) +6:(6) +7:(7) +8:(8) +9:(9) +10:(10) +11:(11) +12:(12) diff --git a/prism-tests/functionality/import/dice2.tra b/prism-tests/functionality/import/dice2.tra new file mode 100644 index 00000000..e7c1e3af --- /dev/null +++ b/prism-tests/functionality/import/dice2.tra @@ -0,0 +1,21 @@ +13 20 +0 1 0.5 +0 2 0.5 +1 3 0.5 +1 4 0.5 +2 5 0.5 +2 6 0.5 +3 1 0.5 +3 7 0.5 +4 8 0.5 +4 9 0.5 +5 10 0.5 +5 11 0.5 +6 2 0.5 +6 12 0.5 +7 7 1 +8 8 1 +9 9 1 +10 10 1 +11 11 1 +12 12 1 diff --git a/prism/src/prism/ExplicitFiles2ModelInfo.java b/prism/src/prism/ExplicitFiles2ModelInfo.java index 867081e6..beabc80c 100644 --- a/prism/src/prism/ExplicitFiles2ModelInfo.java +++ b/prism/src/prism/ExplicitFiles2ModelInfo.java @@ -102,6 +102,8 @@ public class ExplicitFiles2ModelInfo extends PrismComponent // This way, expressions can refer to the labels later on. if (labelsFile != null) { extractLabelNamesFromLabelsFile(labelsFile); + } else { + labelNames = new ArrayList<>(); } // Set model type: if no preference stated, try to autodetect