Browse Source

Explicit model import bugfix (when no .sta file is provided).

With accompanying regression test. Follows additional fix in last commit.
accumulation-v4.7
Dave Parker 6 years ago
parent
commit
3af9eb9466
  1. 8
      prism-tests/functionality/import/dice2.lab
  2. 3
      prism-tests/functionality/import/dice2.pm.importexport.auto
  3. 8
      prism-tests/functionality/import/dice2.srew
  4. 14
      prism-tests/functionality/import/dice2.sta
  5. 21
      prism-tests/functionality/import/dice2.tra
  6. 2
      prism/src/prism/ExplicitFiles2ModelInfo.java

8
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

3
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

8
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

14
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)

21
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

2
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

Loading…
Cancel
Save