From b362047e4f5b3379dc48293e01eb8073b26c9e92 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 2 Sep 2016 01:06:35 +0200 Subject: [PATCH] mutex example Former-commit-id: 6e249da5941f21fab093a0af1442b18e9ecbc589 --- examples/multiobjective/ma/mutex/mutex2.ma | 93 +++++++++++++++++ examples/multiobjective/ma/mutex/mutex3.ma | 98 ++++++++++++++++++ examples/multiobjective/ma/mutex/mutex4.ma | 103 +++++++++++++++++++ examples/multiobjective/ma/mutex/mutex5.ma | 110 +++++++++++++++++++++ 4 files changed, 404 insertions(+) create mode 100644 examples/multiobjective/ma/mutex/mutex2.ma create mode 100644 examples/multiobjective/ma/mutex/mutex3.ma create mode 100644 examples/multiobjective/ma/mutex/mutex4.ma create mode 100644 examples/multiobjective/ma/mutex/mutex5.ma diff --git a/examples/multiobjective/ma/mutex/mutex2.ma b/examples/multiobjective/ma/mutex/mutex2.ma new file mode 100644 index 000000000..296afa8ec --- /dev/null +++ b/examples/multiobjective/ma/mutex/mutex2.ma @@ -0,0 +1,93 @@ +// Translation of the MAPA Specification of a mutex system into PRISM code +// http://wwwhome.cs.utwente.nl/~timmer/scoop/papers/qest13/index.html + +ma + +const int N; // The size of the data (should be at most 6) + +formula someEnter = s1=1 | s2=1; +formula someWait = s1=2 | s2=2; +formula someLow = s1=3 | s2=3; +formula someHigh = s1=4 | s2=4; +formula someTie = s1=5 | s2=5; +formula someAdmit = s1=6 | s2=6; +formula otherHigh = s2=4; + +formula someLowTie = someLow | someTie; +formula someLowHighTie = someLow | someHigh | someTie; +formula someAdmitHighTie = someAdmit | someHigh | someTie; +formula someEnterWait = someEnter | someWait; + + +module process1 + + // The internal state of the process + // 0: uninterested + // 1: enter + // 2: wait + // 3: low + // 4: high + // 5: tie + // 6: admit + s1 : [0..6]; + + // the phase of the protocol + phase1 : [1..12]; + + // The considered data + data1 : [1..N]; + + // The result of a coin flip + h1 : bool; + + //[] phase1=1 -> 1 : true; + [] phase1=1 -> 1 : (phase1'=2); + + [] phase1=2 & N>=1 -> 1 : (data1'=1) & (phase1'=3); + [] phase1=2 & N>=2 -> 1 : (data1'=2) & (phase1'=3); + [] phase1=2 & N>=3 -> 1 : (data1'=3) & (phase1'=3); + [] phase1=2 & N>=4 -> 1 : (data1'=4) & (phase1'=3); + [] phase1=2 & N>=5 -> 1 : (data1'=5) & (phase1'=3); + [] phase1=2 & N>=6 -> 1 : (data1'=6) & (phase1'=3); + + [] phase1=3 & (someLowHighTie & !someAdmit) -> 1 : (s1'=2) & (phase1'=4); + [] phase1=3 & (!someLowHighTie | someAdmit) -> 0.5 : (phase1'=5) & (h1'=false) + 0.5 : (phase1'=5) & (h1'=true); + + [] phase1=4 & (!someLowHighTie | someAdmit) -> 1 : (s1'=1) & (phase1'=3); + + [] phase1=5 & h1=false -> 1 : (s1'=3) & (phase1'=6); + [] phase1=5 & h1=true -> 1 : (s1'=4) & (phase1'=7) & (h1'=false); + + [] phase1=6 & !someAdmitHighTie -> 1 : (s1'=5) & (phase1'=8); + + [] phase1=7 & (someAdmit | otherHigh) -> 1 : (s1'=5) & (phase1'=9); + [] phase1=7 & (!someAdmit & !otherHigh) -> 1 : (phase1'=10); + + [] phase1=8 -> 0.5 : (phase1'=5) & (h1'=false) + 0.5 : (phase1'=5) & (h1'=true); + + [] phase1=9 & !someAdmit & !otherHigh -> 0.5 : (phase1'=5) & (h1'=false) + 0.5 : (phase1'=5) & (h1'=true); + + <> phase1=10 -> data1 : (phase1'=11) & (data1'=1); + + [] phase1=11 & (someLowTie | otherHigh) & !someEnter -> 1 : (s1'=0) & (phase1'=1); + [] phase1=11 & !someLowTie & !otherHigh -> 1 : (s1'=6) & (phase1'=12); + + [] phase1=12 & !someEnterWait -> 1 : (s1'=0) & (phase1'=1); + +endmodule + +module process2 = process1 [ s1=s2, phase1=phase2, data1=data2, h1=h2, s2=s1] endmodule + +label "crit1" = phase1=10; +label "crit2" = phase2=10; + + +rewards "timeInCrit1" + phase1=10 : 1; +endrewards + + +rewards "timeInCrit2" + phase2=10 : 1; +endrewards + diff --git a/examples/multiobjective/ma/mutex/mutex3.ma b/examples/multiobjective/ma/mutex/mutex3.ma new file mode 100644 index 000000000..f47ef31f5 --- /dev/null +++ b/examples/multiobjective/ma/mutex/mutex3.ma @@ -0,0 +1,98 @@ +// Translation of the MAPA Specification of a mutex system into PRISM code +// http://wwwhome.cs.utwente.nl/~timmer/scoop/papers/qest13/index.html + +ma + +const int N; // The size of the data (should be at most 6) + +formula someEnter = s1=1 | s2=1 | s3=1; +formula someWait = s1=2 | s2=2 | s3=2; +formula someLow = s1=3 | s2=3 | s3=3; +formula someHigh = s1=4 | s2=4 | s3=4; +formula someTie = s1=5 | s2=5 | s3=5; +formula someAdmit = s1=6 | s2=6 | s3=6; +formula otherHigh = s2=4 | s3=4; + +formula someLowTie = someLow | someTie; +formula someLowHighTie = someLow | someHigh | someTie; +formula someAdmitHighTie = someAdmit | someHigh | someTie; +formula someEnterWait = someEnter | someWait; + + +module process1 + + // The internal state of the process + // 0: uninterested + // 1: enter + // 2: wait + // 3: low + // 4: high + // 5: tie + // 6: admit + s1 : [0..6]; + + // the phase of the protocol + phase1 : [1..12]; + + // The considered data + data1 : [1..N]; + + // The result of a coin flip + h1 : bool; + + //[] phase1=1 -> 1 : true; + [] phase1=1 -> 1 : (phase1'=2); + + [] phase1=2 & N>=1 -> 1 : (data1'=1) & (phase1'=3); + [] phase1=2 & N>=2 -> 1 : (data1'=2) & (phase1'=3); + [] phase1=2 & N>=3 -> 1 : (data1'=3) & (phase1'=3); + [] phase1=2 & N>=4 -> 1 : (data1'=4) & (phase1'=3); + [] phase1=2 & N>=5 -> 1 : (data1'=5) & (phase1'=3); + [] phase1=2 & N>=6 -> 1 : (data1'=6) & (phase1'=3); + + [] phase1=3 & (someLowHighTie & !someAdmit) -> 1 : (s1'=2) & (phase1'=4); + [] phase1=3 & (!someLowHighTie | someAdmit) -> 0.5 : (phase1'=5) & (h1'=false) + 0.5 : (phase1'=5) & (h1'=true); + + [] phase1=4 & (!someLowHighTie | someAdmit) -> 1 : (s1'=1) & (phase1'=3); + + [] phase1=5 & h1=false -> 1 : (s1'=3) & (phase1'=6); + [] phase1=5 & h1=true -> 1 : (s1'=4) & (phase1'=7) & (h1'=false); + + [] phase1=6 & !someAdmitHighTie -> 1 : (s1'=5) & (phase1'=8); + + [] phase1=7 & (someAdmit | otherHigh) -> 1 : (s1'=5) & (phase1'=9); + [] phase1=7 & (!someAdmit & !otherHigh) -> 1 : (phase1'=10); + + [] phase1=8 -> 0.5 : (phase1'=5) & (h1'=false) + 0.5 : (phase1'=5) & (h1'=true); + + [] phase1=9 & !someAdmit & !otherHigh -> 0.5 : (phase1'=5) & (h1'=false) + 0.5 : (phase1'=5) & (h1'=true); + + <> phase1=10 -> data1 : (phase1'=11) & (data1'=1); + + [] phase1=11 & (someLowTie | otherHigh) & !someEnter -> 1 : (s1'=0) & (phase1'=1); + [] phase1=11 & !someLowTie & !otherHigh -> 1 : (s1'=6) & (phase1'=12); + + [] phase1=12 & !someEnterWait -> 1 : (s1'=0) & (phase1'=1); + +endmodule + +module process2 = process1 [ s1=s2, phase1=phase2, data1=data2, h1=h2, s2=s1] endmodule +module process3 = process1 [ s1=s3, phase1=phase3, data1=data3, h1=h3, s3=s1] endmodule + +label "crit1" = phase1=10; +label "crit2" = phase2=10; +label "crit3" = phase3=10; + + +rewards "timeInCrit1" + phase1=10 : 1; +endrewards + +rewards "timeInCrit2" + phase2=10 : 1; +endrewards + +rewards "timeInCrit3" + phase3=10 : 1; +endrewards + diff --git a/examples/multiobjective/ma/mutex/mutex4.ma b/examples/multiobjective/ma/mutex/mutex4.ma new file mode 100644 index 000000000..8068933ef --- /dev/null +++ b/examples/multiobjective/ma/mutex/mutex4.ma @@ -0,0 +1,103 @@ +// Translation of the MAPA Specification of a mutex system into PRISM code +// http://wwwhome.cs.utwente.nl/~timmer/scoop/papers/qest13/index.html + +ma + +const int N; // The size of the data (should be at most 6) + +formula someEnter = s1=1 | s2=1 | s3=1 | s4=1; +formula someWait = s1=2 | s2=2 | s3=2 | s4=2; +formula someLow = s1=3 | s2=3 | s3=3 | s4=3; +formula someHigh = s1=4 | s2=4 | s3=4 | s4=4; +formula someTie = s1=5 | s2=5 | s3=5 | s4=5; +formula someAdmit = s1=6 | s2=6 | s3=6 | s4=6; +formula otherHigh = s2=4 | s3=4 | s4=4; + +formula someLowTie = someLow | someTie; +formula someLowHighTie = someLow | someHigh | someTie; +formula someAdmitHighTie = someAdmit | someHigh | someTie; +formula someEnterWait = someEnter | someWait; + + +module process1 + + // The internal state of the process + // 0: uninterested + // 1: enter + // 2: wait + // 3: low + // 4: high + // 5: tie + // 6: admit + s1 : [0..6]; + + // the phase of the protocol + phase1 : [1..12]; + + // The considered data + data1 : [1..N]; + + // The result of a coin flip + h1 : bool; + + //[] phase1=1 -> 1 : true; + [] phase1=1 -> 1 : (phase1'=2); + + [] phase1=2 & N>=1 -> 1 : (data1'=1) & (phase1'=3); + [] phase1=2 & N>=2 -> 1 : (data1'=2) & (phase1'=3); + [] phase1=2 & N>=3 -> 1 : (data1'=3) & (phase1'=3); + [] phase1=2 & N>=4 -> 1 : (data1'=4) & (phase1'=3); + [] phase1=2 & N>=5 -> 1 : (data1'=5) & (phase1'=3); + [] phase1=2 & N>=6 -> 1 : (data1'=6) & (phase1'=3); + + [] phase1=3 & (someLowHighTie & !someAdmit) -> 1 : (s1'=2) & (phase1'=4); + [] phase1=3 & (!someLowHighTie | someAdmit) -> 0.5 : (phase1'=5) & (h1'=false) + 0.5 : (phase1'=5) & (h1'=true); + + [] phase1=4 & (!someLowHighTie | someAdmit) -> 1 : (s1'=1) & (phase1'=3); + + [] phase1=5 & h1=false -> 1 : (s1'=3) & (phase1'=6); + [] phase1=5 & h1=true -> 1 : (s1'=4) & (phase1'=7) & (h1'=false); + + [] phase1=6 & !someAdmitHighTie -> 1 : (s1'=5) & (phase1'=8); + + [] phase1=7 & (someAdmit | otherHigh) -> 1 : (s1'=5) & (phase1'=9); + [] phase1=7 & (!someAdmit & !otherHigh) -> 1 : (phase1'=10); + + [] phase1=8 -> 0.5 : (phase1'=5) & (h1'=false) + 0.5 : (phase1'=5) & (h1'=true); + + [] phase1=9 & !someAdmit & !otherHigh -> 0.5 : (phase1'=5) & (h1'=false) + 0.5 : (phase1'=5) & (h1'=true); + + <> phase1=10 -> data1 : (phase1'=11) & (data1'=1); + + [] phase1=11 & (someLowTie | otherHigh) & !someEnter -> 1 : (s1'=0) & (phase1'=1); + [] phase1=11 & !someLowTie & !otherHigh -> 1 : (s1'=6) & (phase1'=12); + + [] phase1=12 & !someEnterWait -> 1 : (s1'=0) & (phase1'=1); + +endmodule + +module process2 = process1 [ s1=s2, phase1=phase2, data1=data2, h1=h2, s2=s1] endmodule +module process3 = process1 [ s1=s3, phase1=phase3, data1=data3, h1=h3, s3=s1] endmodule +module process4 = process1 [ s1=s4, phase1=phase4, data1=data4, h1=h4, s4=s1] endmodule + +label "crit1" = phase1=10; +label "crit2" = phase2=10; +label "crit3" = phase3=10; +label "crit4" = phase4=10; + + +rewards "timeInCrit1" + phase1=10 : 1; +endrewards + +rewards "timeInCrit2" + phase2=10 : 1; +endrewards + +rewards "timeInCrit3" + phase3=10 : 1; +endrewards + +rewards "timeInCrit4" + phase4=10 : 1; +endrewards diff --git a/examples/multiobjective/ma/mutex/mutex5.ma b/examples/multiobjective/ma/mutex/mutex5.ma new file mode 100644 index 000000000..2755d829c --- /dev/null +++ b/examples/multiobjective/ma/mutex/mutex5.ma @@ -0,0 +1,110 @@ +// Translation of the MAPA Specification of a mutex system into PRISM code +// http://wwwhome.cs.utwente.nl/~timmer/scoop/papers/qest13/index.html + +ma + +const int N; // The size of the data (should be at most 6) + +formula someEnter = s1=1 | s2=1 | s3=1 | s4=1 | s5=1; +formula someWait = s1=2 | s2=2 | s3=2 | s4=2 | s5=2; +formula someLow = s1=3 | s2=3 | s3=3 | s4=3 | s5=3; +formula someHigh = s1=4 | s2=4 | s3=4 | s4=4 | s5=4; +formula someTie = s1=5 | s2=5 | s3=5 | s4=5 | s5=5; +formula someAdmit = s1=6 | s2=6 | s3=6 | s4=6 | s5=6; +formula otherHigh = s2=4 | s3=4 | s4=4 | s5=4; + +formula someLowTie = someLow | someTie; +formula someLowHighTie = someLow | someHigh | someTie; +formula someAdmitHighTie = someAdmit | someHigh | someTie; +formula someEnterWait = someEnter | someWait; + +module process1 + + // The internal state of the process + // 0: uninterested + // 1: enter + // 2: wait + // 3: low + // 4: high + // 5: tie + // 6: admit + s1 : [0..6]; + + // the phase of the protocol + phase1 : [1..12]; + + // The considered data + data1 : [1..N]; + + // The result of a coin flip + h1 : bool; + + //[] phase1=1 -> 1 : true; + [] phase1=1 -> 1 : (phase1'=2); + + [] phase1=2 & N>=1 -> 1 : (data1'=1) & (phase1'=3); + [] phase1=2 & N>=2 -> 1 : (data1'=2) & (phase1'=3); + [] phase1=2 & N>=3 -> 1 : (data1'=3) & (phase1'=3); + [] phase1=2 & N>=4 -> 1 : (data1'=4) & (phase1'=3); + [] phase1=2 & N>=5 -> 1 : (data1'=5) & (phase1'=3); + [] phase1=2 & N>=6 -> 1 : (data1'=6) & (phase1'=3); + + [] phase1=3 & (someLowHighTie & !someAdmit) -> 1 : (s1'=2) & (phase1'=4); + [] phase1=3 & (!someLowHighTie | someAdmit) -> 0.5 : (phase1'=5) & (h1'=false) + 0.5 : (phase1'=5) & (h1'=true); + + [] phase1=4 & (!someLowHighTie | someAdmit) -> 1 : (s1'=1) & (phase1'=3); + + [] phase1=5 & h1=false -> 1 : (s1'=3) & (phase1'=6); + [] phase1=5 & h1=true -> 1 : (s1'=4) & (phase1'=7) & (h1'=false); + + [] phase1=6 & !someAdmitHighTie -> 1 : (s1'=5) & (phase1'=8); + + [] phase1=7 & (someAdmit | otherHigh) -> 1 : (s1'=5) & (phase1'=9); + [] phase1=7 & (!someAdmit & !otherHigh) -> 1 : (phase1'=10); + + [] phase1=8 -> 0.5 : (phase1'=5) & (h1'=false) + 0.5 : (phase1'=5) & (h1'=true); + + [] phase1=9 & !someAdmit & !otherHigh -> 0.5 : (phase1'=5) & (h1'=false) + 0.5 : (phase1'=5) & (h1'=true); + + <> phase1=10 -> data1 : (phase1'=11) & (data1'=1); + + [] phase1=11 & (someLowTie | otherHigh) & !someEnter -> 1 : (s1'=0) & (phase1'=1); + [] phase1=11 & !someLowTie & !otherHigh -> 1 : (s1'=6) & (phase1'=12); + + [] phase1=12 & !someEnterWait -> 1 : (s1'=0) & (phase1'=1); + +endmodule + +module process2 = process1 [ s1=s2, phase1=phase2, data1=data2, h1=h2, s2=s1] endmodule +module process3 = process1 [ s1=s3, phase1=phase3, data1=data3, h1=h3, s3=s1] endmodule +module process4 = process1 [ s1=s4, phase1=phase4, data1=data4, h1=h4, s4=s1] endmodule +module process5 = process1 [ s1=s5, phase1=phase5, data1=data5, h1=h5, s5=s1] endmodule + + +label "crit1" = phase1=10; +label "crit2" = phase2=10; +label "crit3" = phase3=10; +label "crit4" = phase4=10; +label "crit5" = phase5=10; + + +rewards "timeInCrit1" + phase1=10 : 1; +endrewards + +rewards "timeInCrit2" + phase2=10 : 1; +endrewards + +rewards "timeInCrit3" + phase3=10 : 1; +endrewards + +rewards "timeInCrit4" + phase4=10 : 1; +endrewards + +rewards "timeInCrit5" + phase5=10 : 1; +endrewards +