Skip to content

Commit 691253b

Browse files
stevanastevana
committedJan 2, 2025
feat: add TPTL experiment
1 parent e070223 commit 691253b

File tree

3 files changed

+183
-3
lines changed

3 files changed

+183
-3
lines changed
 

‎spex.cabal

+1
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,7 @@ library
4242
Spex.Experiment.Protocol
4343
Spex.Experiment.Protocol2
4444
Spex.Experiment.Protocol3
45+
Spex.Experiment.TimedPropositionalTemporalLogic
4546
Spex.Generator.Arbitrary
4647
Spex.Generator.Combinator
4748
Spex.Generator.Prng

‎src/Spex/Experiment/Grammar.hs

+4-3
Original file line numberDiff line numberDiff line change
@@ -7,13 +7,14 @@ import Control.Monad
77
import Data.List (intersect)
88
import Data.String
99

10-
import Spex.Verifier.Generator
11-
import Spex.Generator.Prng
1210
import Spex.Generator.Combinator
11+
import Spex.Generator.Prng
12+
import Spex.Verifier.Generator
1313

1414
-- https://www.cse.chalmers.se/~coquand/AUTOMATA/w6.html
1515
-- https://en.wikipedia.org/wiki/Augmented_Backus%E2%80%93Naur_form
1616
-- https://en.wikipedia.org/wiki/Extended_Backus%E2%80%93Naur_form
17+
-- https://matt.might.net/articles/regular-context-free-grammars/
1718

1819
------------------------------------------------------------------------
1920

@@ -137,7 +138,7 @@ gen re | notEmpty re = case re of
137138
Inter e1 e2 -> intersect <$> gen e1 <*> gen e2
138139

139140
prop_gen :: (Monoid a, Eq a) => Int -> Size -> Reg a -> Bool
140-
prop_gen seed size re =
141+
prop_gen seed size re =
141142
snd (runGen (gen re) (mkPrng seed) size) `isIn` re
142143

143144
testRe :: Reg Char

‎src/Spex/Experiment/TimedPropositionalTemporalLogic.hs

+178
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,178 @@
1+
module Spex.Experiment.TimedPropositionalTemporalLogic (module Spex.Experiment.TimedPropositionalTemporalLogic) where
2+
3+
-- TPLT from "A Really Temporal Logic" (1994):
4+
-- https://www.seas.upenn.edu/~alur/JACM94.pdf
5+
6+
import Data.Fixed
7+
import Data.Map.Strict (Map)
8+
import Data.Map.Strict qualified as Map
9+
import Data.Maybe
10+
import Data.Time
11+
import Data.Time.Clock.POSIX
12+
import Numeric.Natural
13+
14+
------------------------------------------------------------------------
15+
16+
infixl 6 :+
17+
infix 4 :<=
18+
19+
type Var = String
20+
21+
-- TODO: Currently the natural stands for seconds, we probably want something
22+
-- smaller to be able to be more precise.
23+
data Constraint
24+
= Var :+ Natural
25+
| RelativeTime Natural
26+
27+
data Form a
28+
= TT
29+
| FF
30+
| Prop (a -> Bool)
31+
| Neg (Form a)
32+
| X (Form a)
33+
| U (Form a) (Form a)
34+
| Always (Form a)
35+
| Eventually (Form a)
36+
| Or (Form a) (Form a)
37+
| And (Form a) (Form a)
38+
| Constraint :<= Constraint
39+
| Congurent Constraint Constraint Natural -- XXX: I'm not sure how to use this...
40+
| FreezeQuantifier Var (Form a)
41+
42+
-- <>x.(p /\ x <= 10)
43+
example :: Form Bool
44+
example =
45+
Eventually $
46+
FreezeQuantifier "x" $
47+
Prop (== True) `And` ("x" :+ 0 :<= RelativeTime 10)
48+
49+
type Env time = Map Var time
50+
51+
class Time t where
52+
(.==) :: t -> t -> Bool
53+
(.<=) :: t -> t -> Bool
54+
(.+) :: t -> Natural -> t
55+
(.-) :: t -> t -> t
56+
(.%) :: t -> Natural -> t
57+
fromNatural :: Natural -> t
58+
59+
instance Time Natural where
60+
t0 .== t1 = t0 == t1
61+
t0 .<= t1 = t0 <= t1
62+
t0 .+ t1 = t0 + t1
63+
t0 .- t1 = t0 - t1
64+
t0 .% t1 = t0 `mod` t1
65+
fromNatural = id
66+
67+
instance Time UTCTime where
68+
t0 .== t1 = t0 == t1
69+
t0 .<= t1 = t0 <= t1
70+
t0 .+ n = fromIntegral n `addUTCTime` t0
71+
t0 .- t1 = posixSecondsToUTCTime (t0 `diffUTCTime` t1)
72+
t0 .% n =
73+
posixSecondsToUTCTime $
74+
secondsToNominalDiffTime $
75+
nominalDiffTimeToSeconds (utcTimeToPOSIXSeconds t0)
76+
`mod'` fromIntegral n
77+
fromNatural = posixSecondsToUTCTime . fromIntegral
78+
79+
-- NOTE: We need t0 here in order to compute the relative time to when the
80+
-- trace started. For time := Natural isn't not needed as t0 = 0, but for
81+
-- timestamps we need the supply the start time.
82+
lookupEnv :: (Time time) => Constraint -> Env time -> time
83+
lookupEnv (x :+ c) env = env Map.! x .+ c
84+
lookupEnv (RelativeTime c) env = env Map.! "t0" .+ fromNatural c
85+
86+
-- TODO: Would be interesting to generalise this from a single trace to lists
87+
-- of traces, and make assertions about percentiles, e.g. a request is always
88+
-- eventually responded to within 200ms in p99, i.e. 1% of requests may be
89+
-- slower.
90+
91+
sat ::
92+
(Time time) =>
93+
Form a
94+
-> [(time, a)]
95+
-> Env time
96+
-> Bool
97+
sat TT _w _env = True
98+
sat FF _w _env = False
99+
sat (Prop p) w _env = p (snd (w !! 0))
100+
sat (Neg p) w env = not (sat p w env)
101+
sat (X p) w env = sat p (drop 1 w) env
102+
sat (U p q) w env =
103+
case listToMaybe [i | i <- [0 .. length w - 1], sat q (drop i w) env] of
104+
Nothing -> False
105+
Just i -> and [sat p (drop k w) env | k <- [0 .. i - 1]]
106+
sat (Always p) w env = and [sat p (drop i w) env | i <- [0 .. length w - 1]]
107+
sat (Eventually p) w env = or [sat p (drop i w) env | i <- [0 .. length w - 1]]
108+
sat (Or p q) w env = sat p w env || sat q w env
109+
sat (And p q) w env = sat p w env && sat q w env
110+
sat (c1 :<= c2) _w env = lookupEnv c1 env .<= lookupEnv c2 env
111+
-- XXX: Not sure if Congurent is right, or how to use it, or if it works with
112+
-- timestamps as opposed to naturals as time...
113+
sat (Congurent c1 c2 d) _w env = (lookupEnv c1 env .- lookupEnv c2 env) .% d .== fromNatural 0
114+
sat (FreezeQuantifier x p) w env = sat p w (Map.insert x t0 env)
115+
where
116+
t0 = fst (w !! 0)
117+
118+
------------------------------------------------------------------------
119+
120+
test0 :: Bool
121+
test0 =
122+
sat
123+
example
124+
( [(0, False), (1, False), (2, False), (9, False), (10, True)] ::
125+
[(Natural, Bool)]
126+
)
127+
(Map.singleton "t0" 0)
128+
== True
129+
130+
test1 :: Bool
131+
test1 =
132+
sat
133+
example
134+
( [(0, False), (1, False), (2, False), (9, False), (11, True)] ::
135+
[(Natural, Bool)]
136+
)
137+
(Map.singleton "t0" 0)
138+
== False
139+
140+
test2 :: IO Bool
141+
test2 = do
142+
now <- getCurrentTime
143+
let t1 = now .+ 1
144+
t2 = now .+ 2
145+
t9 = now .+ 9
146+
t10 = now .+ 10
147+
print now
148+
print t1
149+
print t10
150+
return $
151+
sat
152+
example
153+
[(now, False), (t1, False), (t2, False), (t9, False), (t10, True)]
154+
(Map.singleton "t0" now)
155+
== True
156+
157+
test3 :: IO Bool
158+
test3 = do
159+
now <- getCurrentTime
160+
let t1 = now .+ 1
161+
t2 = now .+ 2
162+
t9 = now .+ 9
163+
t11 = now .+ 11
164+
print now
165+
print t11
166+
return $
167+
sat
168+
example
169+
[(now, False), (t1, False), (t2, False), (t9, False), (t11, True)]
170+
(Map.singleton "t0" now)
171+
== False
172+
173+
test :: IO ()
174+
test = do
175+
b2 <- test2
176+
b3 <- test3
177+
let bools = [test0, test1, b2, b3]
178+
if and bools then putStrLn "Passed" else print bools

0 commit comments

Comments
 (0)