-
Notifications
You must be signed in to change notification settings - Fork 0
/
TemporalDemo.hs
39 lines (27 loc) · 1.14 KB
/
TemporalDemo.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
{-# LANGUAGE TemplateHaskell #-}
module TemporalDemo where
-- Implement temporal logic by parameterising explicitly on a stream of events.
import Logical
import NameTree
import Numerals
import NamedReqs
now :: Requirement a -> Requirement [a]
now r = $(matching [| \xs -> anonymous $ boolean $ not (null xs) |]) #&&
$(matching [| \(x:_) -> r `onValue` x |])
next :: Requirement [a] -> Requirement [a]
next r = $(matching [| \xs -> anonymous $ boolean $ not (null xs) |]) #&&
$(matching [| \(_:xs) -> r `onValue` xs |])
end :: Requirement [a]
end = $(matching [| \xs -> anonymous $ boolean $ null xs |])
-------------
inRange =
$(matching [| \n ->
named "inRange" . group roman $
(named "lowerBound" . boolean $ n >= 0)
#&& (named "upperBound" . withError (show n ++" > 100") $ boolean $ n <= 100)
|])
always r = recursively $ \rec -> end #|| (r #>&& next rec)
eventually r = recursively $ \rec -> r #>|| next rec
-- Hmm. Covering eventually r is tricky... it requires a stream in
-- which r holds ONLY ONCE. Not sure this is really what we want for
-- POSITIVE coverage.