HOA path formulas

prism-tests/functionality/verify/dtmcs/hoa/GFa_and_FGb_parity.hoa

@@ -0,0 +1,31 @@
+HOA: v1
+name: "G(Fa & FGb)"
+States: 4
+Start: 0
+AP: 2 "a" "b"
+acc-name: parity max even 2
+Acceptance: 2 Fin(1) & Inf(0)
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic stutter-invariant
+--BODY--
+State: 0 {0 1}
+[0&!1] 0
+[0&1] 1
+[!0&!1] 2
+[!0&1] 3
+State: 1 {0}
+[0&!1] 0
+[0&1] 1
+[!0&!1] 2
+[!0&1] 3
+State: 2 {1}
+[0&!1] 0
+[0&1] 1
+[!0&!1] 2
+[!0&1] 3
+State: 3
+[0&!1] 0
+[0&1] 1
+[!0&!1] 2
+[!0&1] 3
+--END--

prism-tests/functionality/verify/dtmcs/hoa/Xa_buchi.hoa

@@ -0,0 +1,20 @@
+HOA: v1
+name: "Xa"
+States: 4
+Start: 1
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic terminal
+--BODY--
+State: 0
+[0] 2
+[!0] 3
+State: 1
+[t] 0
+State: 2 {0}
+[t] 2
+State: 3
+[t] 3
+--END--

prism-tests/functionality/verify/dtmcs/hoa/lec15dtmc.pm

@@ -0,0 +1,16 @@
+// Simple DTMC from Lec 15 of Probabilistic Model Checking
+
+dtmc
+
+module M
+
+s:[0..5];
+
+[] s=0 -> 0.5:(s'=1) + 0.5:(s'=3);
+[] s=1 -> 0.5:(s'=0) + 0.25:(s'=2) + 0.25:(s'=4);
+[] s=2 -> 1:(s'=5);
+[] s=3 -> 1:(s'=3);
+[] s=4 -> 1:(s'=4);
+[] s=5 -> 1:(s'=2);
+
+endmodule

prism-tests/functionality/verify/dtmcs/hoa/lec15dtmc.pm.hoa.props

@@ -0,0 +1,47 @@
+// explicitly resolve path via $PROPERTY_DIR
+// RESULT: 1/6
+P=?[ HOA: { "$PROPERTY_DIR/GFa_and_FGb_parity.hoa", "a" <- s=2, "b" <- s=2|s=5} ]
+
+// explicitly resolve path via $MODEL_DIR
+// RESULT: 1/6
+P=?[ HOA: { "$MODEL_DIR/GFa_and_FGb_parity.hoa", "a" <- s=2, "b" <- s=2|s=5} ]
+
+// from now on, implicitly resolve via property dir
+
+// RESULT: 1/6
+P=?[ HOA: { "GFa_and_FGb_parity.hoa", "a" <- s=2, "b" <- s=2|s=5} ]
+// RESULT: 1/6
+P=?[ (G F s=2) & (F G (s=2|s=5)) ]
+
+// RESULT: 5/6
+P=?[ ! HOA: { "GFa_and_FGb_parity.hoa", "a" <- s=2, "b" <- s=2|s=5} ]
+// RESULT: 5/6
+P=?[ !((G F s=2) & (F G (s=2|s=5))) ]
+
+
+// RESULT: 5/6
+P=?[ HOA: { "GFa_and_FGb_parity.hoa", "a" <- s>=2, "b" <- s>=3} ]
+// RESULT: 5/6
+P=?[ (G F s>=2) & (F G s>=3) ]
+// RESULT: 1/6
+P=?[ ! HOA: { "GFa_and_FGb_parity.hoa", "a" <- s>=2, "b" <- s>=3} ]
+// RESULT: 1/6
+P=?[ !((G F s>=2) & (F G s>=3)) ]
+
+// use labels directly as APs for the automaton
+label "a" = s>=2;
+label "b" = s>=3;
+// RESULT: 5/6
+P=?[ HOA: { "GFa_and_FGb_parity.hoa" } ]
+// RESULT: 1/6
+P=?[ ! HOA: { "GFa_and_FGb_parity.hoa" } ]
+
+// RESULT: 1/2
+P=?[ HOA: {"Xa_buchi.hoa"} ]
+// RESULT: 1/2
+P=?[ X "a" ]
+
+// RESULT: 1/2
+P=?[ ! HOA: {"Xa_buchi.hoa"} ]
+// RESULT: 1/2
+P=?[ ! (X "a") ]

prism-tests/functionality/verify/mdps/hoa/GFa_and_FGb.hoa

@@ -0,0 +1,31 @@
+HOA: v1
+name: "G(Fa & FGb)"
+States: 4
+Start: 0
+AP: 2 "a" "b"
+acc-name: parity max even 2
+Acceptance: 2 Fin(1) & Inf(0)
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic stutter-invariant
+--BODY--
+State: 0 {0 1}
+[0&!1] 0
+[0&1] 1
+[!0&!1] 2
+[!0&1] 3
+State: 1 {0}
+[0&!1] 0
+[0&1] 1
+[!0&!1] 2
+[!0&1] 3
+State: 2 {1}
+[0&!1] 0
+[0&1] 1
+[!0&!1] 2
+[!0&1] 3
+State: 3
+[0&!1] 0
+[0&1] 1
+[!0&!1] 2
+[!0&1] 3
+--END--

prism-tests/functionality/verify/mdps/hoa/GFa_and_FGb_rabin.hoa

@@ -0,0 +1,33 @@
+HOA: v1
+name: "G(Fa & FGb)"
+States: 6
+Start: 0
+AP: 2 "a" "b"
+acc-name: Rabin 1
+Acceptance: 2 Fin(0) & Inf(1)
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic stutter-invariant
+--BODY--
+State: 0 {0}
+[!0 | !1] 1
+[0&1] 2
+State: 1
+[!0 | !1] 1
+[0&1] 2
+State: 2
+[!1] 0
+[0&1] 3
+[!0&1] 4
+State: 3 {1}
+[!1] 0
+[0&1] 3
+[!0&1] 4
+State: 4 {1}
+[!1] 0
+[0&1] 3
+[!0&1] 5
+State: 5
+[!1] 0
+[0&1] 3
+[!0&1] 5
+--END--

prism-tests/functionality/verify/mdps/hoa/Xa_buchi.hoa

@@ -0,0 +1,20 @@
+HOA: v1
+name: "Xa"
+States: 4
+Start: 1
+AP: 1 "a"
+acc-name: Buchi
+Acceptance: 1 Inf(0)
+properties: trans-labels explicit-labels state-acc complete
+properties: deterministic terminal
+--BODY--
+State: 0
+[0] 2
+[!0] 3
+State: 1
+[t] 0
+State: 2 {0}
+[t] 2
+State: 3
+[t] 3
+--END--

prism-tests/functionality/verify/mdps/hoa/lec15mdp.nm

@@ -0,0 +1,22 @@
+// Simple MDP from Lec 15 of Probabilistic Model Checking
+
+mdp
+
+module M
+
+s:[0..8];
+
+[] s=0 -> 1:(s'=2);
+[] s=0 -> 0.6:(s'=0) + 0.3:(s'=1) + 0.1:(s'=2);
+[] s=1 -> 0.3:(s'=3) + 0.7:(s'=4);
+[] s=3 -> 1:(s'=4);
+[] s=4 -> 1:(s'=1);
+[] s=4 -> 1:(s'=3);
+[] s=4 -> 1:(s'=6);
+[] s=6 -> 1:(s'=6);
+[] s=2 -> 1:(s'=5);
+[] s=5 -> 0.9:(s'=7) + 0.1:(s'=8);
+[] s=7 -> 1:(s'=5);
+[] s=8 -> 1:(s'=5);
+
+endmodule

prism-tests/functionality/verify/mdps/hoa/lec15mdp.nm.hoa.props

@@ -0,0 +1,33 @@
+// RESULT: 3/4
+Pmax=?[ HOA: { "GFa_and_FGb_rabin.hoa", "a" <- s>=3, "b" <- s<=4} ]
+// RESULT: 3/4
+Pmax=?[ (G F s>=3) & (F G (s<=4)) ]
+
+// RESULT: 0
+Pmin=?[ HOA: { "GFa_and_FGb_rabin.hoa", "a" <- s>=3, "b" <- s<=4} ]
+// RESULT: 0
+Pmin=?[ (G F s>=3) & (F G (s<=4)) ]
+
+// RESULT: 0
+1 - Pmax=?[ ! HOA: { "GFa_and_FGb_rabin.hoa", "a" <- s>=3, "b" <- s<=4} ]
+// RESULT: 0
+1 - Pmax=?[ !((G F s>=3) & (F G (s<=4))) ]
+
+// use labels directly as APs for the automaton
+label "a" = s>=3;
+label "b" = s<=4;
+// RESULT: 3/4
+Pmax=?[ HOA: { "GFa_and_FGb_rabin.hoa" } ]
+
+
+// RESULT: 0.3
+Pmax=?[ HOA: { "Xa_buchi.hoa", "a" <- s=1 } ]
+// RESULT: 0.3
+Pmax=?[ X s=1 ]
+
+// RESULT: 0
+Pmin=?[ HOA: { "Xa_buchi.hoa", "a" <- s=1 } ]
+// RESULT: 0
+Pmin=?[ X s=1 ]
+
+