-
Notifications
You must be signed in to change notification settings - Fork 0
/
Examples.hs
74 lines (64 loc) · 2.67 KB
/
Examples.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
module Examples where
import Control.Monad(forM_)
import Data.Set(singleton)
import Core
{- Kripke structure from page 179. -}
kripkeS_example = KS (2, r, l)
where
r 0 = [1, 2]
r 1 = [0, 2]
r 2 = [2]
l 0 = \a -> elem a ["p", "q"]
l 1 = \a -> elem a ["q", "r"]
l 2 = (== "r")
{- LTL examples from page 182. -}
ltl_examples = [
([0], ConjP (St $ Var "p") (St $ Var "q")),
([0], St $ Neg "r"),
([0], St top),
([0], X $ St $ Var "r"),
([0], X $ ConjP (St $ Var "q") (St $ Var "r")),
([0], opG $ negP $ ConjP (St $ Var "p") (St $ Var "r")),
([2], opG $ St $ Var "r"),
([0, 1, 2], impP (opF $ ConjP (St $ Neg "q") (St $ Var "r")) (opF $ opG $ St $ Var "r")),
([0], opG $ opF $ St $ Var "p"),
([0], impP (opG $ opF $ St $ Var "p") (opG $ opF $ St $ Var "r")),
([0], impP (opG $ opF $ St $ Var "r") (opG $ opF $ St $ Var "p"))
]
{- LTL examples from page 213. -}
ctl_examples = [
(0, ConjS (Var "p") (Var "q")),
(0, Neg "r"),
(0, top),
(0, E $ X $ St $ ConjS (Var "q") (Var "r")),
(0, negS $ A $ X $ St $ ConjS (Var "q") (Var "r")),
(0, negS $ E $ opF $ St $ ConjS (Var "p") (Var "r")),
(2, E $ opG $ St $ Var "r"),
(0, A $ opF $ St $ Var "r"),
(0, E $ U (St $ ConjS (Var "p") (Var "q")) (St $ Var "r")),
(0, A $ U (St $ Var "p") (St $ Var "r")),
(0, A $ opG $ St $ impS (DisyS (DisyS (Var "p") (Var "q")) (Var "r"))
(E $ opF $ St $ E $ opG $ St $ Var "r"))
]
examples::IO ()
examples = do
putStrLn "Kripke Structure:"
putStrLn $ "\tStates: " ++ show [0, 1, 2]
putStrLn $ "\t R(0) = [1, 2]"
putStrLn $ "\t R(1) = [0, 2]"
putStrLn $ "\t R(2) = [2]"
putStrLn $ "\t L(0) = [p, q]"
putStrLn $ "\t L(1) = [q, r]"
putStrLn $ "\t L(2) = [r]"
putStrLn "\n\tLTL EXAMPLES:"
forM_ ltl_examples (\(states, ф) -> do
forM_ states (\s -> do
let σ = Assrt (s, singleton ф)
putStr $ show σ ++ ": "
print $ eval_mcALTL kripkeS_example σ))
putStrLn "\n\tCTL EXAMPLES:"
forM_ ctl_examples (\(s, φ) -> do
putStr $ show (s, φ) ++ ": "
print $ eval_mcCTLS kripkeS_example (s, φ))
putStrLn $ "\nExamples from:"
putStrLn "Michael Huth & Mark Ryan, “LOGIC IN COMPUTER SCIENCE, Modelling and Reasoning about Systems”, Second Edition."