diff --git a/prism-examples/mec-tests/1.pm b/prism-examples/mec-tests/1.pm new file mode 100644 index 00000000..55c1b431 --- /dev/null +++ b/prism-examples/mec-tests/1.pm @@ -0,0 +1,9 @@ +mdp + +module mec_tests + + s : [0..1] init 0; + + [] s=0 -> 1.0 : (s'=0) ; + +endmodule diff --git a/prism-examples/mec-tests/2.pm b/prism-examples/mec-tests/2.pm new file mode 100644 index 00000000..cc273835 --- /dev/null +++ b/prism-examples/mec-tests/2.pm @@ -0,0 +1,11 @@ +mdp + +module mec_tests + + s : [0..1] init 0; + + [] s=0 -> 1.0 : (s'=1) ; + [] s=1 -> 1.0 : (s'=0) ; + + +endmodule diff --git a/prism-examples/mec-tests/3.pm b/prism-examples/mec-tests/3.pm new file mode 100644 index 00000000..bebf016b --- /dev/null +++ b/prism-examples/mec-tests/3.pm @@ -0,0 +1,12 @@ +mdp + +module mec_tests + + s : [0..2] init 0; + + [] s=0 -> 1.0 : (s'=1); + [] s=1 -> 1.0 : (s'=0); + [] s=0 -> 1.0 : (s'=2); + [] s=2 -> 1.0 : (s'=2); + +endmodule diff --git a/prism-examples/mec-tests/4.pm b/prism-examples/mec-tests/4.pm new file mode 100644 index 00000000..101f840e --- /dev/null +++ b/prism-examples/mec-tests/4.pm @@ -0,0 +1,13 @@ +mdp + +module mec_tests + + s : [0..2] init 0; + + [] s=0 -> 1.0 : (s'=1); + [] s=1 -> 1.0 : (s'=0); + [] s=0 -> 1.0 : (s'=2); + [] s=2 -> 1.0 : (s'=2); + [] s=2 -> 1.0 : (s'=1); + +endmodule diff --git a/prism/src/explicit/ECComputerDefault.java b/prism/src/explicit/ECComputerDefault.java index f73c8efa..324dbf16 100644 --- a/prism/src/explicit/ECComputerDefault.java +++ b/prism/src/explicit/ECComputerDefault.java @@ -31,6 +31,8 @@ import java.util.ArrayList; import java.util.BitSet; import java.util.List; +import explicit.SCCComputer.SCCMethod; + /** * Maximal end component computer for a nondeterministic model such as MDP. */ @@ -54,7 +56,17 @@ public class ECComputerDefault extends ECComputer @Override public void computeMECs() { - // TODO + SCCComputer sccc = SCCComputer.createSCCComputer(SCCMethod.TARJAN, model); + sccc.computeSCCs(); + + List sccs = sccc.getSCCs(); + + for(int i=0;i