From 3c09c81c8ea3463b83b7c936109419630a26640d Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 6 Dec 2023 16:42:35 -0800 Subject: [PATCH] Future time LTL. [ci skip] --- CopilotData/Data/Buchi.hs | 62 ++++++++++ CopilotData/Data/DFA.hs | 126 ++++++++++++++++++++ CopilotData/Data/FSM.hs | 18 +++ CopilotData/Data/Graph.hs | 54 +++++++++ CopilotData/Data/LTL.hs | 76 ++++++++++++ CopilotData/Data/LTL3.hs | 239 ++++++++++++++++++++++++++++++++++++++ CopilotData/Data/LTL4.hs | 89 ++++++++++++++ CopilotData/Data/NFA.hs | 22 ++++ CopilotData/Data/State.hs | 70 +++++++++++ Eval.hs | 20 ++++ Incremental.hs | 31 +++++ 11 files changed, 807 insertions(+) create mode 100644 CopilotData/Data/Buchi.hs create mode 100644 CopilotData/Data/DFA.hs create mode 100644 CopilotData/Data/FSM.hs create mode 100644 CopilotData/Data/Graph.hs create mode 100644 CopilotData/Data/LTL.hs create mode 100644 CopilotData/Data/LTL3.hs create mode 100644 CopilotData/Data/LTL4.hs create mode 100644 CopilotData/Data/NFA.hs create mode 100644 CopilotData/Data/State.hs create mode 100644 Eval.hs create mode 100644 Incremental.hs diff --git a/CopilotData/Data/Buchi.hs b/CopilotData/Data/Buchi.hs new file mode 100644 index 000000000..8aedfbc2c --- /dev/null +++ b/CopilotData/Data/Buchi.hs @@ -0,0 +1,62 @@ +module CopilotData.Data.Buchi where + +-- External +import qualified Data.Graph as G +import Data.List ( intersect, sort ) +import Data.Maybe ( catMaybes ) +import Prelude hiding ( mod, (&&), (++), (/=), (<), (==), (>) ) +import qualified Prelude as P + +-- External: Copilot +import Language.Copilot hiding ( not ) + +-- Temporary +import Debug.Trace + +-- Internal +import CopilotData.Data.Graph + +-- * Non-deterministic Buchi automata + +data NBA alphabet state = NBA + { nbaAlphabet :: [alphabet] + , nbaInitialState :: state + , nbaState :: [state] + , nbaTransitions :: [((state, alphabet), [state])] + , nbaFinalStates :: [state] + } + deriving (Eq, Show) + +isLanguageEmpty :: (Eq alphabet, Ord state) => NBA alphabet state -> Bool +isLanguageEmpty nba = not + $ null + $ intersect + (nbaFinalStates nba) + (stronglyConnected nba (nbaInitialState nba)) + +stronglyConnected :: (Eq alphabet, Ord state) => NBA alphabet state -> state -> [state] +stronglyConnected nba s = sort $ concatMap graphStates $ filter (reachable nba s) graphs + where + graphs = stronglyConnectedComponents nba + +stronglyConnectedComponents :: (Eq alphabet, Ord state) => NBA alphabet state -> [Graph state] +stronglyConnectedComponents nba = graphSCCs (nbaToGraph nba) + +reachable :: (Eq alphabet, Ord state) + => NBA alphabet state + -> state + -> Graph state + -> Bool +reachable nba state graph = any (nbaReachable nba state) (graphStates graph) + +nbaReachable :: (Eq alphabet, Ord state) => NBA alphabet state -> state -> state -> Bool +nbaReachable nba s1 s2 = graphPath (nbaToGraph nba) s1 s2 + +nbaToGraph :: (Eq alphabet, Ord state) => NBA alphabet state -> Graph state +nbaToGraph nba = Graph g (nbaState nba) adjacents kf + where + (g, vf, kf) = (G.graphFromEdges adjacents) + adjacents = [ (s, s, ss) + | s <- nbaState nba + , let ss = sort $ concat $ catMaybes $ map (\a -> lookup (s, a) (nbaTransitions nba)) (nbaAlphabet nba) + ] diff --git a/CopilotData/Data/DFA.hs b/CopilotData/Data/DFA.hs new file mode 100644 index 000000000..75d7036c4 --- /dev/null +++ b/CopilotData/Data/DFA.hs @@ -0,0 +1,126 @@ +{-# LANGUAGE RankNTypes #-} +module CopilotData.Data.DFA where + +import Data.List ( sort, nub ) +import Data.Maybe ( fromJust ) +import Prelude as P +import System.IO +import System.IO.Unsafe +import Text.Pretty.Simple (pPrint) + +import CopilotData.Data.NFA + +prettyDebug prefix a = unsafePerformIO $ do + print prefix + pPrint a + hFlush stdout + +test = powerset nfa + +origin :: IO () +origin = pPrint nfa + +nfa = NFA + [0, 1] + ["zero", "one"] + "zero" + [ (("zero", 0),["zero"]) + , (("zero", 1),["one"]) + , (("one", 0), ["one"]) + , (("one", 1), ["one"]) + ] + ["one"] + +nfa2 = NFA + { nfaAlphabet = + [ 0 + , 1 + ] + , nfaStates = + [ 1 + , 0 + ] + , nfaInitialState = 0 + , nfaTransitions = + [ + ( ( 1 , 0) , [ 0 ]) + , + ( ( 1 , 1) , [ 1 ]) + , + ( ( 0 , 0) , [ 1 ]) + , + ( ( 0 , 1) , [ 0 ]) + ] + , nfaFinalStates = [] + } + +-- * Deterministic Finite Automata + +data DFA alphabet state = DFA + { alphabet :: [alphabet] + , states :: [state] + , initialState :: state + , transitions :: [((state, alphabet), state)] + , finalStates :: [state] + } + deriving (Eq, Show) + +powerset :: forall alphabet state + . (Eq alphabet, Ord state, Show state, Show alphabet) + => NFA alphabet state + -> DFA alphabet [state] +powerset nfa = powerset' nfa front s' r' + where + front = [[nfaInitialState nfa]] + s' = [] + r' = [] + +powerset' :: forall alphabet state + . (Eq alphabet, Ord state, Show state, Show alphabet) + => NFA alphabet state + -> [[state]] + -> [[state]] + -> [(([state], alphabet), [state])] + -> DFA alphabet [state] +powerset' nfa [] s' r' = DFA a s i t f + where + -- a :: [alphabet] -- doesn't type check but is correct? + a = nub $ nfaAlphabet nfa + + s = nub s' + + i = [nfaInitialState nfa] + + -- t :: ([state], alphabet) -> [state] + t = nub r' + + f = filter (any (`elem` (nfaFinalStates nfa))) s' + +powerset' nfa (f1:front) s' r' = powerset'' nfa f1 front s'' r' (nfaAlphabet nfa) + where + s'' = nub $ s' P.++ [f1] + +powerset'' :: forall alphabet state + . (Eq alphabet, Ord state, Show state, Show alphabet) + => NFA alphabet state + -> [state] + -> [[state]] + -> [[state]] + -> [(([state], alphabet), [state])] + -> [alphabet] + -> DFA alphabet [state] +powerset'' nfa s front sTilde rTilde [] = powerset' nfa front sTilde rTilde + +powerset'' nfa s front sTilde rTilde (sigma:uSigma) = powerset'' nfa s front' sTilde rTilde' uSigma + where + rTilde' = rTilde P.++ [((s, sigma), s')] + s' = nub $ sort $ concatMap (\state -> mySuccessors nfa state sigma) s + front' = if s' `notElem` sTilde then front P.++ [s'] else front + +mySuccessors nfa state sigma = + let e = successors nfa state sigma + in -- (prettyDebug "mySucc:" (state, sigma, e)) `seq` e + e + +myFromJust Nothing = error "DFAFromJust" +myFromJust x = fromJust x diff --git a/CopilotData/Data/FSM.hs b/CopilotData/Data/FSM.hs new file mode 100644 index 000000000..fabf050fe --- /dev/null +++ b/CopilotData/Data/FSM.hs @@ -0,0 +1,18 @@ +-- * Finite State Machines +module CopilotData.Data.FSM where + +import Text.Pretty.Simple (pPrint) + +-- | Finite State Machines +data FSM alphabet state output = FSM + { fsmAlphabet :: [alphabet] + , fsmStates :: [state] + , fsmInitialState :: state + , fsmTransitions :: [((state, alphabet), state)] + , fsmOutputs :: [output] + , fsmOutputFunction :: [(state, output)] + } + deriving (Eq, Show) + +minimize :: FSM alphabet state output -> FSM alphabet state output +minimize = id diff --git a/CopilotData/Data/Graph.hs b/CopilotData/Data/Graph.hs new file mode 100644 index 000000000..bcd10f901 --- /dev/null +++ b/CopilotData/Data/Graph.hs @@ -0,0 +1,54 @@ +{-# LANGUAGE RankNTypes #-} +-- | Graphs +module CopilotData.Data.Graph where + +import qualified Data.Graph as G + +-- | Graphs that are polymorphic on the type of the state. +data Graph state = Graph + { graphGraph :: G.Graph + , graphStates :: [state] + , graphAdjacency :: [(state, state, [state])] + , graphStateKeys :: state -> Maybe G.Vertex + } + +-- | True if two states are connected in the graph. +graphPath :: Ord state + => Graph state + -> state + -> state + -> Bool +graphPath g s1 s2 + | Just s1' <- graphStateKeys g s1 + , Just s2' <- graphStateKeys g s2 + = G.path (graphGraph g) s1' s2' + + | otherwise + = False + +-- | List all strongly connected components. +graphSCCs :: forall state + . Ord state + => Graph state + -> [Graph state] +graphSCCs graph = map (subgraph graph) $ map G.flattenSCC sccs + where + sccs = G.stronglyConnComp $ graphAdjacency graph + +-- | Narrow a graph to only contain specific states. +subgraph :: Ord state + => Graph state + -> [state] + -> Graph state +subgraph graph states = Graph g s a k + where + g = graphGraph graph + s = states + a = [ (v, v, vs) | (v, _, vs0) <- graphAdjacency graph + , v `elem` states + , let vs = filter (`elem` states) vs0 + , not (null vs) + ] + k s + | s `elem` states = graphStateKeys graph s + | otherwise = Nothing diff --git a/CopilotData/Data/LTL.hs b/CopilotData/Data/LTL.hs new file mode 100644 index 000000000..46ee5efb5 --- /dev/null +++ b/CopilotData/Data/LTL.hs @@ -0,0 +1,76 @@ +module CopilotData.Data.LTL where + +import Data.List ( nub, sort ) +import Prelude hiding ( mod, (&&), (++), (/=), (<), (==), (>) ) +import qualified Prelude as P + +data LTLFormula = LTLTrue + | LTLProp Int + | LTLNot LTLFormula + | LTLAnd LTLFormula LTLFormula + | LTLUntil LTLFormula LTLFormula + | LTLNext LTLFormula + deriving (Eq, Ord, Show) + +ltlEventually :: LTLFormula -> LTLFormula +ltlEventually = LTLUntil LTLTrue + +ltlGlobally :: LTLFormula -> LTLFormula +ltlGlobally = LTLNot . ltlEventually . LTLNot + +ltlOr :: LTLFormula -> LTLFormula -> LTLFormula +ltlOr x y = LTLNot (LTLNot x `LTLAnd` LTLNot y) + +ltlFalse :: LTLFormula +ltlFalse = LTLNot LTLTrue + +allProps :: LTLFormula -> [Int] +allProps (LTLTrue) = [] +allProps (LTLProp x) = [x] +allProps (LTLNot x) = allProps x +allProps (LTLAnd x1 x2) = allProps x1 P.++ allProps x2 +allProps (LTLUntil x1 x2) = allProps x1 P.++ allProps x2 +allProps (LTLNext x) = allProps x + +subformulas :: LTLFormula -> [LTLFormula] +subformulas = nub . sort . subformulas' + +subformulas' :: LTLFormula -> [LTLFormula] +subformulas' f@LTLTrue = [f] +subformulas' f@(LTLProp _) = [f] +subformulas' f@(LTLNot fi) = f : subformulas' fi +subformulas' f@(LTLAnd fi1 fi2) = f : (subformulas' fi1 P.++ subformulas' fi2) +subformulas' f@(LTLUntil fi1 fi2) = f : (subformulas' fi1 P.++ subformulas' fi2) +subformulas' f@(LTLNext fi) = f : subformulas' fi + +-- * Tests + +formula1 :: LTLFormula +formula1 = LTLTrue + +formula2 :: LTLFormula +formula2 = LTLNot LTLTrue + +formula3 :: LTLFormula +formula3 = LTLAnd formula1 formula2 + +formula4 :: LTLFormula +formula4 = LTLUntil formula1 formula3 + +formula5 :: LTLFormula +formula5 = LTLNext formula4 + +formula6 :: LTLFormula +formula6 = LTLProp 55 + +allFormulas :: [ LTLFormula ] +allFormulas = [ formula1 + , formula2 + , formula3 + , formula4 + , formula5 + , formula6 + ] + +test1 :: IO () +test1 = mapM_ (print . subformulas) allFormulas diff --git a/CopilotData/Data/LTL3.hs b/CopilotData/Data/LTL3.hs new file mode 100644 index 000000000..d57d6d0bf --- /dev/null +++ b/CopilotData/Data/LTL3.hs @@ -0,0 +1,239 @@ +{-# LANGUAGE RankNTypes #-} +module CopilotData.Data.LTL3 where +import Data.List ( lookup, nub, sort ) +import Data.Maybe ( fromJust, maybeToList ) +import Debug.Trace +import Language.Copilot hiding ( not ) +import Prelude hiding ( mod, (&&), (++), (/=), (<), (==), + (>) ) +import qualified Prelude as P +import System.IO +import System.IO.Unsafe +import Text.Pretty.Simple (pPrint) + +import CopilotData.Data.Buchi +import qualified CopilotData.Data.DFA as DFA +import CopilotData.Data.FSM +import CopilotData.Data.LTL +import CopilotData.Data.NFA +import CopilotData.Data.State + +-- * Three valued logic +type Bool3 = Word8 + +true3 :: Bool3 +true3 = 1 + +unknown3:: Bool3 +unknown3 = 2 + +false3 :: Bool3 +false3 = 3 + +prettyDebug prefix a = unsafePerformIO $ do + print prefix + pPrint a + hFlush stdout + +-- Given a formula phi, monitor is: +monitor :: [(Int, Stream Bool)] -> LTLFormula -> Stream Bool3 +monitor streams psi = fsmToMonitor streams $ minimize $ prod + where + prod = -- unsafePerformIO (pPrint prod') `seq` + prod' + prod' = productDFA psi + +fsmToMonitor :: [(Int, Stream Bool)] + -> FSM [Int] ([LTLFormula], [LTLFormula]) Bool3 + -> Stream Bool3 +fsmToMonitor streams fsm = + stateMachineGF $ toStateMachine streams fsm + +toStateMachine :: [(Int, Stream Bool)] + -> FSM [Int] ([LTLFormula], [LTLFormula]) Bool3 + -> StateMachineGF +toStateMachine inputs fsm = + prettyDebug "Graph:" g `seq` g + where + g = (initial, 255, false, transitions, 255, outputMapping) + alphabet = fsmAlphabet fsm + states = zip (fsmStates fsm) [0..] + initial = myFromJust $ lookup (fsmInitialState fsm) states + transitions = [ (sn, e, sn') + + | ((s, input), s') <- fsmTransitions fsm + + , let sn :: Word8 + sn = myFromJust $ lookup s states + + , let sn' :: Word8 + sn' = myFromJust $ lookup s' states + + , let u :: [Int] + u = input + + , let e = conforms inputs input + + ] + + outputMapping = [(sn, on) | (s, sn) <- states + , on <- map snd $ filter ((s P.==).fst) (fsmOutputFunction fsm) + ] + + conforms :: [(Int, Stream Bool)] -> [Int] -> Stream Bool + conforms inputStreams inputs = + streamAll $ map snd $ filter (\(k, v) -> k `elem` inputs) inputStreams + where + streamAll [] = true + streamAll (x:xs) = x && streamAll xs + +productDFA :: LTLFormula -> FSM [Int] ([LTLFormula], [LTLFormula]) Bool3 +productDFA psi = r + where + r = FSM sigma qbar q0bar deltabar [true3, false3, unknown3] lambdabar + + sigma :: [[Int]] + sigma = DFA.alphabet a1 + + qbar = [(s1, s2) | s1 <- DFA.states a1, s2 <- DFA.states a2 ] + q0bar = (DFA.initialState a1, DFA.initialState a2) + deltabar = [ ( ((q, q'), a) + , (x, y) + ) + | (q, q') <- qbar + , a <- DFA.alphabet a1 + , x <- map snd $ filter (((q, a) P.==).fst) $ DFA.transitions a1 + , y <- map snd $ filter (((q', a) P.==).fst) $ DFA.transitions a2 + ] + + -- I think the bug is here + lambdabar = [ ((q, q'), false3) + | (q, q') <- qbar + , q `notElem` DFA.finalStates a1 + ] + + P.++ + + [ ((q, q'), true3) + | (q, q') <- qbar + , q' `notElem` DFA.finalStates a2 + ] + + P.++ + + [ ((q, q'), unknown3) + | (q, q') <- qbar + , q' `elem` DFA.finalStates a1 P.&& q' `elem` DFA.finalStates a2 + ] + + a1 :: DFA.DFA [Int] [LTLFormula] + a1 = dfaFromStream psi + + a2 :: DFA.DFA [Int] [LTLFormula] + a2 = dfaFromStream (LTLNot psi) + +dfaFromStream :: LTLFormula -> DFA.DFA [Int] [LTLFormula] +dfaFromStream l = -- (prettyDebug "DFA from stream: " (r, n)) `seq` r + r + where + r = DFA.powerset n + n = nfaFromStream l + +nfaFromStream :: LTLFormula -> NFA [Int] LTLFormula +nfaFromStream psi = r -- (prettyDebug "NFA: " r) `seq` r + where + r = NFA a ss s0 d f + a = nbaAlphabet nba + ss = nbaState nba + s0 = nbaInitialState nba + d = nbaTransitions nba + f = [ q | q <- nbaFinalStates $ nba, curlyF psi q ] + + curlyF psi s = isLanguageEmpty (nba { nbaInitialState = s }) + + nba = nbaFromStream psi + +nbaFromStream :: LTLFormula -> NBA [Int] LTLFormula +nbaFromStream formula = -- (prettyDebug "NBA: " r) `seq` r + r + -- r + where + r = NBA + { nbaAlphabet = alphabet + , nbaInitialState = formula + , nbaState = states + , nbaTransitions = trans' + , nbaFinalStates = [ s | s@(LTLNot (x1 `LTLUntil` x2)) <- states ] + } + + alphabet = sublists $ allProps formula + + states = sort $ nub $ map reduceNots $ subformulas formula P.++ subformulas (LTLNot formula) + P.++ [LTLTrue, LTLNot LTLTrue] + -- states' = sort $ nub $ states P.++ filter (\x -> x == LTLTrue \/ x == LTLNot LTLTrue) (map snd trans') + + trans' :: [((LTLFormula, [Int]), [LTLFormula])] + trans' = [ ((x, a), s) | x <- states, a <- alphabet, let s = trans (x, a) ] + + trans :: (LTLFormula, [Int]) -> [LTLFormula] + trans (LTLProp i, a) = [ if i `elem` a then LTLTrue else ltlFalse ] + trans (LTLTrue, _) = [] + trans (LTLNot f, a) = map complement' (trans (f, a)) + trans (LTLAnd p1 p2, a) = [ LTLAnd v1 v2 | v1 <- trans (p1, a), + v2 <- trans (p2, a)] + trans (LTLUntil p1 p2, a) = [ ltlOr v1 v3 | v1 <- trans (p1, a) + , v2 <- trans (p2, a) + , let v3 = LTLAnd v2 (LTLUntil p1 p2) + ] + trans (LTLNext p1, _) = [ p1 ] + +reduceNots :: LTLFormula -> LTLFormula +reduceNots (LTLNot (LTLNot x)) = reduceNots x +reduceNots (LTLNot f) = LTLNot (reduceNots f) +reduceNots (LTLAnd f1 f2) = LTLAnd (reduceNots f1) (reduceNots f2) +reduceNots (LTLUntil f1 f2) = LTLUntil (reduceNots f1) (reduceNots f2) +reduceNots (LTLNext f) = LTLNext (reduceNots f) +reduceNots f = f + +complement' :: LTLFormula -> LTLFormula +complement' = reduceNots . complement'' . reduceNots + +complement'' LTLTrue = ltlFalse +complement'' (LTLAnd x1 x2) = ltlOr (complement'' x1) (complement'' x2) +complement'' (LTLNot (LTLNot x1 `LTLAnd` LTLNot x2)) = LTLAnd (complement'' x1) (complement'' x2) +complement'' (LTLNot (x1 `LTLAnd` x2)) = LTLAnd (complement'' (LTLNot x1)) (complement'' (LTLNot x2)) +complement'' (LTLNot (LTLNot x1)) = LTLNot (complement'' x1) +complement'' x1 = LTLNot x1 + +-- * Auxiliary + +-- | List all sublists of a list. +sublists :: [a] -> [[a]] +sublists [] = [[]] +sublists (x:xs) = remainder P.++ map (x:) remainder + where + remainder = sublists xs + +testNBA = nbaFromStream (LTLProp 55) +testNFA = nfaFromStream (LTLProp 55) + +-- -- myTrans' :: [((LTLFormula, [Int]), [LTLFormula])] +-- myTrans' states alphabet = [ ((x, a), s) | x <- states, a <- alphabet, let s = myTrans states alphabet (x, a) ] +-- +-- -- myTrans :: (LTLFormula, [Int]) -> [LTLFormula] +-- myTrans states alphabet (LTLProp i, a) = [ if i `elem` a then LTLTrue else ltlFalse ] +-- myTrans states alphabet (LTLTrue, _) = [] +-- myTrans states alphabet (LTLNot f, a) = let e = (myTrans states alphabet (f, a)) +-- e' = map complement' e +-- in trace ("This: " P.++ show (e, e')) $ e' +-- myTrans states alphabet (LTLAnd p1 p2, a) = [ LTLAnd v1 v2 | v1 <- myTrans states alphabet (p1, a), +-- v2 <- myTrans states alphabet (p2, a)] +-- myTrans states alphabet (LTLUntil p1 p2, a) = [ ltlOr v1 v3 | v1 <- myTrans states alphabet (p1, a) +-- , v2 <- myTrans states alphabet (p2, a) +-- , let v3 = LTLAnd v2 (LTLUntil p1 p2) +-- ] +-- myTrans states alphabet (LTLNext p1, _) = [ p1 ] +-- +-- +myFromJust Nothing = error "LTL3FromJust" +myFromJust x = fromJust x diff --git a/CopilotData/Data/LTL4.hs b/CopilotData/Data/LTL4.hs new file mode 100644 index 000000000..4e52edc4f --- /dev/null +++ b/CopilotData/Data/LTL4.hs @@ -0,0 +1,89 @@ +{-# LANGUAGE RankNTypes #-} +module CopilotData.Data.LTL4 where +import Control.Monad +import Copilot.Compile.C99 +import qualified Data.Graph as G +import Data.List ( intersect, lookup, nub, sort ) +import Data.Maybe ( catMaybes, fromJust ) +import Data.Tuple ( swap ) +import Debug.Trace +import Language.Copilot hiding ( not ) +import Prelude hiding ( mod, (&&), (++), (/=), (<), (==), + (>) ) +import qualified Prelude as P + +type Result = Int8 + +absTrue :: Result +absTrue = 2 + +soFarTrue :: Result +soFarTrue = 1 + +soFarFalse :: Result +soFarFalse = -1 + +absFalse :: Result +absFalse = -2 + +negate' :: Stream Result -> Stream Result +negate' s = 0 - s + +and' :: Stream Result -> Stream Result -> Stream Result +and' s1 s2 = mux (s1 < s2) s1 s2 + +or' :: Stream Result -> Stream Result -> Stream Result +or' s1 s2 = mux (s1 > s2) s1 s2 + +implies' :: Stream Result -> Stream Result -> Stream Result +implies' s1 s2 = negate' s1 `or'` s2 + +globally' :: Stream Result -> Stream Result +globally' s = mux (s > 0) (constant soFarTrue) s + +eventually' :: Stream Result -> Stream Result +eventually' s = go + where + go = mux (s == 2) s +-- $ mux (s == 1) s + $ before + before = [soFarFalse] ++ go + +example :: Stream Result +example = extern "example" (Just [absTrue, absTrue, absFalse]) + +example2 :: Stream Result +example2 = extern "example" (Just [absFalse, absTrue, absFalse]) + +example3 :: Stream Result +example3 = extern "example" (Just [absFalse, absTrue, absTrue]) + +-- spec :: Spec +-- spec = do +-- observer "globally" (globally' example2) +-- observer "example 1" (eventually' example2) +-- observer "example 2" (eventually' (globally' example2)) +-- observer "example 3" (eventually' (globally' example3)) + +-- main :: IO () +-- main = do +-- spec' <- reify spec +-- interpret 3 spec + +data Prop = PConst Result + | PStream (Stream Bool) + | PNot Prop + | PAnd Prop Prop + | POr Prop Prop + | PImplies Prop Prop + | PGlobally Prop + | PEventually Prop + +eval :: Prop -> Stream Result +eval (PConst r) = constant r +eval (PNot r) = negate' (eval r) +eval (PAnd r1 r2) = and' (eval r1) (eval r2) +eval (POr r1 r2) = or' (eval r1) (eval r2) +eval (PImplies r1 r2) = implies' (eval r1) (eval r2) +eval (PGlobally r) = globally' (eval r) +eval (PEventually r) = eventually' (eval r) diff --git a/CopilotData/Data/NFA.hs b/CopilotData/Data/NFA.hs new file mode 100644 index 000000000..797ac2fe1 --- /dev/null +++ b/CopilotData/Data/NFA.hs @@ -0,0 +1,22 @@ +-- | Non-deterministic Finite Automata +module CopilotData.Data.NFA where + +import Data.List ( lookup ) +import Data.Maybe ( fromMaybe ) + +-- * Non-deterministic Finite Automata +data NFA alphabet state = NFA + { nfaAlphabet :: [alphabet] + , nfaStates :: [state] + , nfaInitialState :: state + , nfaTransitions :: [((state, alphabet), [state])] + , nfaFinalStates :: [state] + } + deriving (Eq, Show) + +successors :: (Eq alphabet, Eq state) + => NFA alphabet state -> state -> alphabet -> [state] +successors nfa state alphabet = concat + $ map snd + $ filter (((state, alphabet) ==).fst) + $ nfaTransitions nfa diff --git a/CopilotData/Data/State.hs b/CopilotData/Data/State.hs new file mode 100644 index 000000000..64bf514b7 --- /dev/null +++ b/CopilotData/Data/State.hs @@ -0,0 +1,70 @@ +module CopilotData.Data.State where + +import Prelude hiding ( mod, (&&), (++), (==), (/=) ) + +import Language.Copilot + +-- Initial state, final state, no transition signal, transitions, bad state +type StateMachineGF = + (Word8, Word8, Stream Bool, [(Word8, Stream Bool, Word8)], Word8, [(Word8, Word8)]) + +stateMachineGF :: StateMachineGF -> Stream Word8 +stateMachineGF (initialState, finalState, noInputData, transitions, badState, outputMapping) = + mapOutput 255 state outputMapping + where + state = [initialState] ++ ifThenElses transitions + + ifThenElses :: [(Word8, Stream Bool, Word8)] -> Stream Word8 + ifThenElses [] = + ifThenElse (state == constant finalState && noInputData) + (constant finalState) + (constant badState) + + ifThenElses ((s1, i, s2):ss) = + ifThenElse (state == constant s1 && i) (constant s2) (ifThenElses ss) + +-- | Apply a map to a stream. +mapOutput :: Word8 -> Stream Word8 -> [(Word8, Word8)] -> Stream Word8 +mapOutput def s [] = constant def +mapOutput def s ((k, v):xs) = + ifThenElse (s == constant k) + (constant v) + (mapOutput def s xs) + +input = extern "inputs" $ Just [1, 2, 2, 2, 1, 1] + +-- Using our API +stateMachine1GF :: Stream Word8 +stateMachine1GF = stateMachineGF (initialState, finalState, noInputs, transitions, badState, mapping) + where + initialState :: Word8 + initialState = 1 + + finalState :: Word8 + finalState = 4 + + noInputs :: Stream Bool + noInputs = noneOf input [1, 2] + + transitions = [ (1, input == 1, 2) + , (2, input == 2, 3) + , (3, input == 2, 3) + , (3, input == 1, 4) + ] + + badState :: Word8 + badState = 5 + + mapping = map (\x -> (x, x)) [1..5] + +noneOf :: Stream Word8 -> [Word8] -> Stream Bool +noneOf input [] = true +noneOf input (x:xs) = input /= constant x && noneOf input xs + +testGraph1GF :: IO () +testGraph1GF = do + interpret 6 spec + +spec :: Spec +spec = do + trigger "values" true [ arg stateMachine1GF ] diff --git a/Eval.hs b/Eval.hs new file mode 100644 index 000000000..0b448d97e --- /dev/null +++ b/Eval.hs @@ -0,0 +1,20 @@ +import Prelude hiding ( mod, (&&), (++), (/=), (<), (==), (>) ) + +import Copilot.Compile.C99 +import Language.Copilot hiding ( not ) + +import CopilotData.Data.LTL +import CopilotData.Data.LTL3 + +main :: IO () +main = do + interpret 10 spec + spec' <- reify spec + compile "c99" spec' + +spec :: Spec +spec = do + trigger "values" true [arg $ monitor [(55, values)] (ltlGlobally (LTLProp 55))] + +values :: Stream Bool +values = extern "values" (Just [ True, True, False, True, False, True, True, False, True, False, True ]) diff --git a/Incremental.hs b/Incremental.hs new file mode 100644 index 000000000..d8b000b73 --- /dev/null +++ b/Incremental.hs @@ -0,0 +1,31 @@ + +-- Approach at RV with LTL by Bauer at al. +main :: IO () +main = do + interpret 50 spec + spec' <- reify spec + compile "c99" spec' + +spec :: Spec +spec = do + observer "formula" (monitor [] (ltlGlobally LTLTrue)) + observer "counter" count + observer "max" currentMax + observer "oddities" oddities + trigger "out" true [arg $ monitor [] (LTLTrue `LTLUntil` LTLTrue)] + + +-- Interesting example of the power of Copilot +count = mux (previousCounter == (1 :: Stream Word8)) + (previousMax + 1) + (previousCounter - 1) + +currentMax = mux (previousCounter == 1) + (previousMax + 1) + previousMax + +previousCounter = [1] ++ count + +previousMax = [0] ++ currentMax + +oddities = currentMax `mod` 2 /= 0