module FSM.Logic (
    -- * Definition of the CTL language
    CTL (..),
    
    -- * Implementation of the model checking algorithm for CTL
    checkCTL
    
) where

import FSM.States
import FSM.Automata

import Data.Set
import qualified Data.Map as Map

-- | This is the definition of the CTL language. More info about this language can be found <https://en.wikipedia.org/wiki/Computation_tree_logic here>. You can find the details of the constructors in the definition of the 'CTL' data.
--
--
-- Here you can find a visual explanation of the constructors defined below.
-- <<https://i.imgur.com/e4tPiOY.jpg CTL examples>>
--
-- <https://www.researchgate.net/figure/CTL-tree-logic-1_fig6_257343964 Source>: A SAFE COTS-BASED DESIGN FLOW OF EMBEDDED SYSTEMS by Salam Hajjar
--

data CTL a = Atom a -- ^ It defines an atomic statement. E.g.:     'Atom' @"The plants look great."@
        | Not (CTL a) --  'Not' negates a 'CTL' formula.
        | And (CTL a) (CTL a) --  'And' 
        | Or (CTL a) (CTL a)
        | EX (CTL a) -- ^ 'EX' means that the 'CTL' formula holds in at least one of the inmediate successors states.
        | EF (CTL a) -- ^ 'EF' means that the 'CTL' formula holds in at least one of the future states.
        | EG (CTL a) -- ^ 'EG' means that the 'CTL' formula holds always from one of the future states.
        | AX (CTL a) -- ^ 'AX' means that the 'CTL' formula holds in every one of the inmediate successors states.
        | AF (CTL a) -- ^ 'AF' means that the 'CTL' formula holds in at least one state of every possible path.
        | AG (CTL a) -- ^ 'AG' means that the 'CTL' formula holds in the current states and all the successors in all paths. (It is true globally)
        | EU (CTL a) (CTL a) -- ^ 'EU' means that exists a path from the current state that satisfies the first 'CTL' formula /until/ it reaches a state in that path that satisfies the second 'CTL' formula.
        | AU (CTL a) (CTL a) -- ^ 'AU' means that every path from the current state satisfies the first 'CTL' formula /until/ it reaches a state that satisfies the second 'CTL' formula.
        deriving (Eq (CTL a)
Eq (CTL a) =>
(CTL a -> CTL a -> Ordering)
-> (CTL a -> CTL a -> Bool)
-> (CTL a -> CTL a -> Bool)
-> (CTL a -> CTL a -> Bool)
-> (CTL a -> CTL a -> Bool)
-> (CTL a -> CTL a -> CTL a)
-> (CTL a -> CTL a -> CTL a)
-> Ord (CTL a)
CTL a -> CTL a -> Bool
CTL a -> CTL a -> Ordering
CTL a -> CTL a -> CTL a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (CTL a)
forall a. Ord a => CTL a -> CTL a -> Bool
forall a. Ord a => CTL a -> CTL a -> Ordering
forall a. Ord a => CTL a -> CTL a -> CTL a
min :: CTL a -> CTL a -> CTL a
$cmin :: forall a. Ord a => CTL a -> CTL a -> CTL a
max :: CTL a -> CTL a -> CTL a
$cmax :: forall a. Ord a => CTL a -> CTL a -> CTL a
>= :: CTL a -> CTL a -> Bool
$c>= :: forall a. Ord a => CTL a -> CTL a -> Bool
> :: CTL a -> CTL a -> Bool
$c> :: forall a. Ord a => CTL a -> CTL a -> Bool
<= :: CTL a -> CTL a -> Bool
$c<= :: forall a. Ord a => CTL a -> CTL a -> Bool
< :: CTL a -> CTL a -> Bool
$c< :: forall a. Ord a => CTL a -> CTL a -> Bool
compare :: CTL a -> CTL a -> Ordering
$ccompare :: forall a. Ord a => CTL a -> CTL a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (CTL a)
Ord,Int -> CTL a -> ShowS
[CTL a] -> ShowS
CTL a -> String
(Int -> CTL a -> ShowS)
-> (CTL a -> String) -> ([CTL a] -> ShowS) -> Show (CTL a)
forall a. Show a => Int -> CTL a -> ShowS
forall a. Show a => [CTL a] -> ShowS
forall a. Show a => CTL a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CTL a] -> ShowS
$cshowList :: forall a. Show a => [CTL a] -> ShowS
show :: CTL a -> String
$cshow :: forall a. Show a => CTL a -> String
showsPrec :: Int -> CTL a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> CTL a -> ShowS
Show)

instance Eq a => Eq (CTL a) where
    (Atom a :: a
a) == :: CTL a -> CTL a -> Bool
== (Atom b :: a
b) = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b
    (Not a :: CTL a
a) == (Not b :: CTL a
b) = CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
b
    (And a :: CTL a
a b :: CTL a
b) == (And c :: CTL a
c d :: CTL a
d) = (CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
c) Bool -> Bool -> Bool
&& (CTL a
b CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
d)
    (Or a :: CTL a
a b :: CTL a
b) == (Or c :: CTL a
c d :: CTL a
d) = (CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
c) Bool -> Bool -> Bool
&& (CTL a
b CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
d)
    (EX a :: CTL a
a) == (EX b :: CTL a
b) = CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
b
    (EF a :: CTL a
a) == (EF b :: CTL a
b) = CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
b
    (EG a :: CTL a
a) == (EG b :: CTL a
b) = CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
b
    (AX a :: CTL a
a) == (AX b :: CTL a
b) = CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
b
    (AF a :: CTL a
a) == (AF b :: CTL a
b) = CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
b
    (AG a :: CTL a
a) == (AG b :: CTL a
b) = CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
b
    (EU a :: CTL a
a b :: CTL a
b) == (EU c :: CTL a
c d :: CTL a
d) = (CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
c) Bool -> Bool -> Bool
&& (CTL a
b CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
d)
    (AU a :: CTL a
a b :: CTL a
b) == (AU c :: CTL a
c d :: CTL a
d) = (CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
c) Bool -> Bool -> Bool
&& (CTL a
b CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
d)
    -- Aditional equivalences
    (Or a :: CTL a
a b :: CTL a
b) == (Not (And (Not c :: CTL a
c) (Not d :: CTL a
d))) = (CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
c) Bool -> Bool -> Bool
&& (CTL a
b CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
d)
    (And a :: CTL a
a b :: CTL a
b) == (Not (Or (Not c :: CTL a
c) (Not d :: CTL a
d))) = (CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
c) Bool -> Bool -> Bool
&& (CTL a
b CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
d)
    
    (AX a :: CTL a
a) == (Not (EX (Not b :: CTL a
b))) = CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
b
    (AF a :: CTL a
a) == (Not (EX (Not b :: CTL a
b))) = CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
b
    (AG a :: CTL a
a) == (Not (EX (Not b :: CTL a
b))) = CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
b
    
    (EX a :: CTL a
a) == (Not (AX (Not b :: CTL a
b))) = CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
b
    (EF a :: CTL a
a) == (Not (AX (Not b :: CTL a
b))) = CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
b
    (EG a :: CTL a
a) == (Not (AX (Not b :: CTL a
b))) = CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
b
    
    (AU a :: CTL a
a b :: CTL a
b) == Not (Or (EU (Not c1 :: CTL a
c1) (Not (Or d :: CTL a
d c2 :: CTL a
c2))) (EG (Not c3 :: CTL a
c3))) = (CTL a
a CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
d) Bool -> Bool -> Bool
&& (CTL a
b CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
c1) Bool -> Bool -> Bool
&& (CTL a
c1 CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
c2) Bool -> Bool -> Bool
&& (CTL a
c2 CTL a -> CTL a -> Bool
forall a. Eq a => a -> a -> Bool
== CTL a
c3)
   
--
-- A(phi) = ¬ E (¬ phi)
             
-- Derived operators
{-
andCTL :: CTL a -> CTL a -> CTL a
andCTL p q = Not (Or (Not p) (Not q))

orCTL :: CTL a -> CTL a -> CTL a
orCTL p q = Not (And (Not p) (Not q))

aX :: CTL a -> CTL a
aX q = Not (EX (Not q))

aF :: CTL a -> CTL a
aF q = Not (EF (Not q))

aG :: CTL a -> CTL a
aG q = Not (EG (Not q))

aU :: CTL a -> CTL a -> CTL a 
aU p q = Not (orCTL (EU (Not q) (Not (orCTL p q))) (EG (Not q)))
-}
--A[φUψ] == ¬( E[(¬ψ)U¬(φ∨ψ)] ∨ EG(¬ψ) )

-- | This is the function that implements the model checking algorithm for CTL as defined by Queille, Sifakis, Clarke, Emerson and Sistla <https://dl.acm.org/doi/abs/10.1145/5397.5399 here> and that was later improved. 
--
-- This function takes as an argument a 'CTL' formula, an 'Automata' and information about the states as defined in "FSM.Automata" and "FSM.States" respectively and checks whether the 'Automata' implies the 'CTL' formula. Once the algorithm has finished, you just need to look at the value in the initial state of the automata to know if it does, for example with:
--
-- @
-- Map.lookup (getInitialState 'Automata') (checkCTL 'CTL' 'Automata' 'AutomataInfo')
-- @ 
--
checkCTL :: Eq a => CTL a -> Automata -> AutomataInfo (CTL a) -> Map.Map Int Bool
checkCTL :: CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool
checkCTL (Atom a :: a
a) tom :: Automata
tom info :: AutomataInfo (CTL a)
info = 
    let states :: [Int]
states = (Set Int -> [Int]
forall a. Set a -> [a]
toList (Automata -> Set Int
getStates Automata
tom))
    in CTL a
-> AutomataInfo (CTL a)
-> Automata
-> [Int]
-> Map Int Bool
-> Map Int Bool
forall a.
Eq a =>
CTL a
-> AutomataInfo (CTL a)
-> Automata
-> [Int]
-> Map Int Bool
-> Map Int Bool
checkCTLaux (a -> CTL a
forall a. a -> CTL a
Atom a
a) AutomataInfo (CTL a)
info Automata
tom [Int]
states ([(Int, Bool)] -> Map Int Bool
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Int
x,Bool
True) | Int
x <- [Int]
states])
checkCTL (Not a :: CTL a
a) tom :: Automata
tom info :: AutomataInfo (CTL a)
info = Map Int Bool -> Map Int Bool
notMap (CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool
forall a.
Eq a =>
CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool
checkCTL CTL a
a Automata
tom AutomataInfo (CTL a)
info)
checkCTL (And a :: CTL a
a b :: CTL a
b) tom :: Automata
tom info :: AutomataInfo (CTL a)
info = Map Int Bool -> Map Int Bool -> Map Int Bool
andMap (CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool
forall a.
Eq a =>
CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool
checkCTL CTL a
a Automata
tom AutomataInfo (CTL a)
info) (CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool
forall a.
Eq a =>
CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool
checkCTL CTL a
b Automata
tom AutomataInfo (CTL a)
info)
checkCTL (EX a :: CTL a
a) tom :: Automata
tom info :: AutomataInfo (CTL a)
info =
    let states :: [Int]
states = (Set Int -> [Int]
forall a. Set a -> [a]
toList (Automata -> Set Int
getStates Automata
tom))
    in CTL a
-> AutomataInfo (CTL a)
-> Automata
-> [Int]
-> Map Int Bool
-> Map Int Bool
forall a.
Eq a =>
CTL a
-> AutomataInfo (CTL a)
-> Automata
-> [Int]
-> Map Int Bool
-> Map Int Bool
checkCTLaux (CTL a -> CTL a
forall a. CTL a -> CTL a
EX CTL a
a) AutomataInfo (CTL a)
info Automata
tom [Int]
states ([(Int, Bool)] -> Map Int Bool
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Int
x,Bool
False) | Int
x <- [Int]
states])
checkCTL (EU a :: CTL a
a b :: CTL a
b) tom :: Automata
tom info :: AutomataInfo (CTL a)
info = 
    let sublabel1 :: Map Int Bool
sublabel1 = CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool
forall a.
Eq a =>
CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool
checkCTL CTL a
a Automata
tom AutomataInfo (CTL a)
info
        sublabel2 :: Map Int Bool
sublabel2 = CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool
forall a.
Eq a =>
CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool
checkCTL CTL a
b Automata
tom AutomataInfo (CTL a)
info
        states :: [Int]
states = (Set Int -> [Int]
forall a. Set a -> [a]
toList (Automata -> Set Int
getStates Automata
tom))
        init_list :: [Int]
init_list = [Int
x | (x :: Int
x,k :: Bool
k) <- (Map Int Bool -> [(Int, Bool)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Int Bool
sublabel2), Bool
k Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
True]
    in CTL a
-> AutomataInfo (CTL a)
-> Automata
-> Map Int Bool
-> Map Int Bool
-> [Int]
-> Map Int Bool
-> Map Int Bool
forall a.
CTL a
-> AutomataInfo (CTL a)
-> Automata
-> Map Int Bool
-> Map Int Bool
-> [Int]
-> Map Int Bool
-> Map Int Bool
checkCTLauxEU (CTL a -> CTL a -> CTL a
forall a. CTL a -> CTL a -> CTL a
EU CTL a
a CTL a
b) AutomataInfo (CTL a)
info Automata
tom ([(Int, Bool)] -> Map Int Bool
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Int
x,Bool
False) | Int
x <- [Int]
states]) ([(Int, Bool)] -> Map Int Bool
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Int
x,Bool
False) | Int
x <- [Int]
states]) [Int]
init_list Map Int Bool
sublabel1
checkCTL (AU a :: CTL a
a b :: CTL a
b) tom :: Automata
tom info :: AutomataInfo (CTL a)
info = 
    let sublabel1 :: Map Int Bool
sublabel1 = CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool
forall a.
Eq a =>
CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool
checkCTL CTL a
a Automata
tom AutomataInfo (CTL a)
info
        sublabel2 :: Map Int Bool
sublabel2 = CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool
forall a.
Eq a =>
CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool
checkCTL CTL a
b Automata
tom AutomataInfo (CTL a)
info
        states :: [Int]
states = (Set Int -> [Int]
forall a. Set a -> [a]
toList (Automata -> Set Int
getStates Automata
tom))
        degree_map :: Map Int Int
degree_map = [(Int, Int)] -> Map Int Int
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Int
x,[Int] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Set Int -> [Int]
forall a. Set a -> [a]
toList (Automata -> Int -> Set Int
getOutgoingStates Automata
tom Int
x))) | Int
x <- [Int]
states]
        label_map :: Map Int Bool
label_map = ([(Int, Bool)] -> Map Int Bool
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Int
x,Bool
False) | Int
x <- [Int]
states])
        init_list :: [Int]
init_list = [Int
x | (x :: Int
x,k :: Bool
k) <- (Map Int Bool -> [(Int, Bool)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Int Bool
sublabel2), Bool
k Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
True]
    in CTL a
-> AutomataInfo (CTL a)
-> Automata
-> Map Int Bool
-> Map Int Int
-> [Int]
-> Map Int Bool
-> Map Int Bool
forall a.
CTL a
-> AutomataInfo (CTL a)
-> Automata
-> Map Int Bool
-> Map Int Int
-> [Int]
-> Map Int Bool
-> Map Int Bool
checkCTLauxAU (CTL a -> CTL a -> CTL a
forall a. CTL a -> CTL a -> CTL a
AU CTL a
a CTL a
b) AutomataInfo (CTL a)
info Automata
tom Map Int Bool
label_map Map Int Int
degree_map [Int]
init_list Map Int Bool
sublabel1
    

checkCTLaux :: Eq a => CTL a -> AutomataInfo (CTL a) -> Automata -> [State] ->  Map.Map Int Bool -> Map.Map Int Bool
checkCTLaux :: CTL a
-> AutomataInfo (CTL a)
-> Automata
-> [Int]
-> Map Int Bool
-> Map Int Bool
checkCTLaux (Atom a :: a
a) info :: AutomataInfo (CTL a)
info tom :: Automata
tom [l :: Int
l] label_map :: Map Int Bool
label_map = 
    let content_info :: Map String (CTL a)
content_info = StateInfo (CTL a) -> Map String (CTL a)
forall a. StateInfo a -> Map String a
getStateInfo (AutomataInfo (CTL a) -> Int -> Maybe String -> StateInfo (CTL a)
forall a. AutomataInfo a -> Int -> Maybe String -> StateInfo a
getInfoInState AutomataInfo (CTL a)
info Int
l Maybe String
forall a. Maybe a
Nothing)
        content :: [CTL a]
content = Map String (CTL a) -> [CTL a]
forall k a. Map k a -> [a]
Map.elems Map String (CTL a)
content_info
        new_bool :: Bool
new_bool = CTL a -> [CTL a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (a -> CTL a
forall a. a -> CTL a
Atom a
a) [CTL a]
content
        f :: p -> Maybe Bool
f _ = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
new_bool
        new_map :: Map Int Bool
new_map = (Bool -> Maybe Bool) -> Int -> Map Int Bool -> Map Int Bool
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update Bool -> Maybe Bool
forall p. p -> Maybe Bool
f Int
l Map Int Bool
label_map
    in Map Int Bool
new_map
checkCTLaux (Atom a :: a
a) info :: AutomataInfo (CTL a)
info tom :: Automata
tom (l :: Int
l:ls :: [Int]
ls) label_map :: Map Int Bool
label_map = 
    let content_info :: Map String (CTL a)
content_info = StateInfo (CTL a) -> Map String (CTL a)
forall a. StateInfo a -> Map String a
getStateInfo (AutomataInfo (CTL a) -> Int -> Maybe String -> StateInfo (CTL a)
forall a. AutomataInfo a -> Int -> Maybe String -> StateInfo a
getInfoInState AutomataInfo (CTL a)
info Int
l Maybe String
forall a. Maybe a
Nothing)
        content :: [CTL a]
content = Map String (CTL a) -> [CTL a]
forall k a. Map k a -> [a]
Map.elems Map String (CTL a)
content_info
        new_bool :: Bool
new_bool = CTL a -> [CTL a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (a -> CTL a
forall a. a -> CTL a
Atom a
a) [CTL a]
content
        f :: p -> Maybe Bool
f _ = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
new_bool
        new_map :: Map Int Bool
new_map = (Bool -> Maybe Bool) -> Int -> Map Int Bool -> Map Int Bool
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update Bool -> Maybe Bool
forall p. p -> Maybe Bool
f Int
l Map Int Bool
label_map
    in CTL a
-> AutomataInfo (CTL a)
-> Automata
-> [Int]
-> Map Int Bool
-> Map Int Bool
forall a.
Eq a =>
CTL a
-> AutomataInfo (CTL a)
-> Automata
-> [Int]
-> Map Int Bool
-> Map Int Bool
checkCTLaux (a -> CTL a
forall a. a -> CTL a
Atom a
a) AutomataInfo (CTL a)
info Automata
tom [Int]
ls Map Int Bool
new_map
checkCTLaux (EX a :: CTL a
a) info :: AutomataInfo (CTL a)
info tom :: Automata
tom ls :: [Int]
ls label_map :: Map Int Bool
label_map = 
    let sublabel :: Map Int Bool
sublabel = CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool
forall a.
Eq a =>
CTL a -> Automata -> AutomataInfo (CTL a) -> Map Int Bool
checkCTL CTL a
a Automata
tom AutomataInfo (CTL a)
info --habría que almacenarlo para no hacerlo en cada iteración, pero con ello tendría que o bien crear una función auxiliar extra o añadir otro argumento a esta función auxiliar
    in CTL a
-> AutomataInfo (CTL a)
-> Automata
-> [Int]
-> Map Int Bool
-> Map Int Bool
-> Map Int Bool
forall a.
CTL a
-> AutomataInfo (CTL a)
-> Automata
-> [Int]
-> Map Int Bool
-> Map Int Bool
-> Map Int Bool
checkCTLauxEX (CTL a -> CTL a
forall a. CTL a -> CTL a
EX CTL a
a) AutomataInfo (CTL a)
info Automata
tom [Int]
ls Map Int Bool
label_map Map Int Bool
sublabel



notMap :: Map.Map Int Bool -> Map.Map Int Bool
notMap :: Map Int Bool -> Map Int Bool
notMap label_map :: Map Int Bool
label_map = Map Int Bool -> [Int] -> Map Int Bool
notMapAux Map Int Bool
label_map (Map Int Bool -> [Int]
forall k a. Map k a -> [k]
Map.keys Map Int Bool
label_map)

notMapAux :: Map.Map Int Bool -> [Int] -> Map.Map Int Bool
notMapAux :: Map Int Bool -> [Int] -> Map Int Bool
notMapAux label_map :: Map Int Bool
label_map [l :: Int
l] = 
    let Just old_bool :: Bool
old_bool = Int -> Map Int Bool -> Maybe Bool
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
l Map Int Bool
label_map
        f :: p -> Maybe Bool
f _ = Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Bool
not Bool
old_bool)
        new_map :: Map Int Bool
new_map = (Bool -> Maybe Bool) -> Int -> Map Int Bool -> Map Int Bool
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update Bool -> Maybe Bool
forall p. p -> Maybe Bool
f Int
l Map Int Bool
label_map
    in Map Int Bool
new_map
notMapAux label_map :: Map Int Bool
label_map (l :: Int
l:ls :: [Int]
ls) = 
    let Just old_bool :: Bool
old_bool = Int -> Map Int Bool -> Maybe Bool
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
l Map Int Bool
label_map
        f :: p -> Maybe Bool
f _ = Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool -> Bool
not Bool
old_bool)
        new_map :: Map Int Bool
new_map = (Bool -> Maybe Bool) -> Int -> Map Int Bool -> Map Int Bool
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update Bool -> Maybe Bool
forall p. p -> Maybe Bool
f Int
l Map Int Bool
label_map
    in Map Int Bool -> [Int] -> Map Int Bool
notMapAux Map Int Bool
new_map [Int]
ls
            
andMap :: Map.Map Int Bool -> Map.Map Int Bool -> Map.Map Int Bool
andMap :: Map Int Bool -> Map Int Bool -> Map Int Bool
andMap label_map1 :: Map Int Bool
label_map1 label_map2 :: Map Int Bool
label_map2 = Map Int Bool -> Map Int Bool -> [Int] -> Map Int Bool
andMapAux Map Int Bool
label_map1 Map Int Bool
label_map2 (Map Int Bool -> [Int]
forall k a. Map k a -> [k]
Map.keys Map Int Bool
label_map1)

andMapAux ::  Map.Map Int Bool -> Map.Map Int Bool -> [Int] -> Map.Map Int Bool
andMapAux :: Map Int Bool -> Map Int Bool -> [Int] -> Map Int Bool
andMapAux label_map1 :: Map Int Bool
label_map1 label_map2 :: Map Int Bool
label_map2 [l :: Int
l] = 
    let Just bool1 :: Bool
bool1 = Int -> Map Int Bool -> Maybe Bool
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
l Map Int Bool
label_map1
        Just bool2 :: Bool
bool2 = Int -> Map Int Bool -> Maybe Bool
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
l Map Int Bool
label_map2
        f :: p -> Maybe Bool
f _ = Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool
bool1 Bool -> Bool -> Bool
&& Bool
bool2)
        new_map :: Map Int Bool
new_map = (Bool -> Maybe Bool) -> Int -> Map Int Bool -> Map Int Bool
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update Bool -> Maybe Bool
forall p. p -> Maybe Bool
f Int
l Map Int Bool
label_map1
    in Map Int Bool
new_map
andMapAux label_map1 :: Map Int Bool
label_map1 label_map2 :: Map Int Bool
label_map2 (l :: Int
l:ls :: [Int]
ls) =
    let Just bool1 :: Bool
bool1 = Int -> Map Int Bool -> Maybe Bool
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
l Map Int Bool
label_map1
        Just bool2 :: Bool
bool2 = Int -> Map Int Bool -> Maybe Bool
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
l Map Int Bool
label_map2
        f :: p -> Maybe Bool
f _ = Bool -> Maybe Bool
forall a. a -> Maybe a
Just (Bool
bool1 Bool -> Bool -> Bool
&& Bool
bool2)
        new_map :: Map Int Bool
new_map = (Bool -> Maybe Bool) -> Int -> Map Int Bool -> Map Int Bool
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update Bool -> Maybe Bool
forall p. p -> Maybe Bool
f Int
l Map Int Bool
label_map1
    in Map Int Bool -> Map Int Bool -> [Int] -> Map Int Bool
andMapAux Map Int Bool
new_map Map Int Bool
label_map2 [Int]
ls
    
checkCTLauxEX :: CTL a -> AutomataInfo (CTL a) -> Automata -> [State] ->  Map.Map Int Bool -> Map.Map Int Bool -> Map.Map Int Bool
checkCTLauxEX :: CTL a
-> AutomataInfo (CTL a)
-> Automata
-> [Int]
-> Map Int Bool
-> Map Int Bool
-> Map Int Bool
checkCTLauxEX (EX a :: CTL a
a) info :: AutomataInfo (CTL a)
info tom :: Automata
tom [l :: Int
l] label_map :: Map Int Bool
label_map marked_map :: Map Int Bool
marked_map =
    let connected :: [Int]
connected = Set Int -> [Int]
forall a. Set a -> [a]
toList (Automata -> Int -> Set Int
getOutgoingStates Automata
tom Int
l)
        connected_map :: Map Int Bool
connected_map = (Int -> Bool -> Bool) -> Map Int Bool -> Map Int Bool
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\k :: Int
k _ -> (Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Int
k [Int]
connected)) Map Int Bool
marked_map
        new_bool :: Bool
new_bool = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or (Map Int Bool -> [Bool]
forall k a. Map k a -> [a]
Map.elems Map Int Bool
connected_map)
        f :: p -> Maybe Bool
f _ = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
new_bool
        new_map :: Map Int Bool
new_map = (Bool -> Maybe Bool) -> Int -> Map Int Bool -> Map Int Bool
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update Bool -> Maybe Bool
forall p. p -> Maybe Bool
f Int
l Map Int Bool
label_map
    in Map Int Bool
new_map
checkCTLauxEX (EX a :: CTL a
a) info :: AutomataInfo (CTL a)
info tom :: Automata
tom (l :: Int
l:ls :: [Int]
ls) label_map :: Map Int Bool
label_map marked_map :: Map Int Bool
marked_map =
    let connected :: [Int]
connected = Set Int -> [Int]
forall a. Set a -> [a]
toList (Automata -> Int -> Set Int
getOutgoingStates Automata
tom Int
l)
        connected_map :: Map Int Bool
connected_map = (Int -> Bool -> Bool) -> Map Int Bool -> Map Int Bool
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\k :: Int
k _ -> (Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Int
k [Int]
connected)) Map Int Bool
marked_map
        new_bool :: Bool
new_bool = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or (Map Int Bool -> [Bool]
forall k a. Map k a -> [a]
Map.elems Map Int Bool
connected_map)
        f :: p -> Maybe Bool
f _ = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
new_bool
        new_map :: Map Int Bool
new_map = (Bool -> Maybe Bool) -> Int -> Map Int Bool -> Map Int Bool
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update Bool -> Maybe Bool
forall p. p -> Maybe Bool
f Int
l Map Int Bool
label_map
    in CTL a
-> AutomataInfo (CTL a)
-> Automata
-> [Int]
-> Map Int Bool
-> Map Int Bool
-> Map Int Bool
forall a.
CTL a
-> AutomataInfo (CTL a)
-> Automata
-> [Int]
-> Map Int Bool
-> Map Int Bool
-> Map Int Bool
checkCTLauxEX (CTL a -> CTL a
forall a. CTL a -> CTL a
EX CTL a
a) AutomataInfo (CTL a)
info Automata
tom [Int]
ls Map Int Bool
new_map Map Int Bool
marked_map

checkCTLauxEU :: CTL a -> AutomataInfo (CTL a) -> Automata ->  Map.Map Int Bool -> Map.Map Int Bool -> [State] -> Map.Map Int Bool -> Map.Map Int Bool
checkCTLauxEU :: CTL a
-> AutomataInfo (CTL a)
-> Automata
-> Map Int Bool
-> Map Int Bool
-> [Int]
-> Map Int Bool
-> Map Int Bool
checkCTLauxEU (EU a :: CTL a
a b :: CTL a
b) info :: AutomataInfo (CTL a)
info tom :: Automata
tom label_map :: Map Int Bool
label_map seenbefore_map :: Map Int Bool
seenbefore_map [] sublabel :: Map Int Bool
sublabel = Map Int Bool
label_map
checkCTLauxEU (EU a :: CTL a
a b :: CTL a
b) info :: AutomataInfo (CTL a)
info tom :: Automata
tom label_map :: Map Int Bool
label_map seenbefore_map :: Map Int Bool
seenbefore_map (k :: Int
k:ks :: [Int]
ks) sublabel :: Map Int Bool
sublabel = 
    let previous_states :: [Int]
previous_states = Set Int -> [Int]
forall a. Set a -> [a]
toList (Automata -> Int -> Set Int
getIncomingStates Automata
tom Int
k)
        f :: p -> Maybe Bool
f _ = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
        new_map :: Map Int Bool
new_map = (Bool -> Maybe Bool) -> Int -> Map Int Bool -> Map Int Bool
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update Bool -> Maybe Bool
forall p. p -> Maybe Bool
f Int
k Map Int Bool
label_map
        (added_previous :: [Int]
added_previous,new_seenbefore_map :: Map Int Bool
new_seenbefore_map) = Map Int Bool
-> [Int] -> Map Int Bool -> [Int] -> ([Int], Map Int Bool)
checkEUprevious Map Int Bool
seenbefore_map [Int]
previous_states Map Int Bool
sublabel [Int]
ks
    in CTL a
-> AutomataInfo (CTL a)
-> Automata
-> Map Int Bool
-> Map Int Bool
-> [Int]
-> Map Int Bool
-> Map Int Bool
forall a.
CTL a
-> AutomataInfo (CTL a)
-> Automata
-> Map Int Bool
-> Map Int Bool
-> [Int]
-> Map Int Bool
-> Map Int Bool
checkCTLauxEU (CTL a -> CTL a -> CTL a
forall a. CTL a -> CTL a -> CTL a
EU CTL a
a CTL a
b) AutomataInfo (CTL a)
info Automata
tom Map Int Bool
new_map Map Int Bool
new_seenbefore_map [Int]
added_previous Map Int Bool
sublabel
        
        
        
checkEUprevious :: Map.Map Int Bool -> [State] -> Map.Map Int Bool -> [State] -> ([State],Map.Map Int Bool)
checkEUprevious :: Map Int Bool
-> [Int] -> Map Int Bool -> [Int] -> ([Int], Map Int Bool)
checkEUprevious seenbefore_map :: Map Int Bool
seenbefore_map [] sublabel :: Map Int Bool
sublabel ls :: [Int]
ls = ([Int]
ls,Map Int Bool
seenbefore_map)
checkEUprevious seenbefore_map :: Map Int Bool
seenbefore_map (p :: Int
p:ps :: [Int]
ps) sublabel :: Map Int Bool
sublabel ls :: [Int]
ls 
    | Bool
previous_bool Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
False = 
        let f :: p -> Maybe Bool
f _ = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
            new_seenbefore_map :: Map Int Bool
new_seenbefore_map = (Bool -> Maybe Bool) -> Int -> Map Int Bool -> Map Int Bool
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update Bool -> Maybe Bool
forall p. p -> Maybe Bool
f Int
p Map Int Bool
seenbefore_map
        in if Bool
previous_marked Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
True
            then Map Int Bool
-> [Int] -> Map Int Bool -> [Int] -> ([Int], Map Int Bool)
checkEUprevious Map Int Bool
new_seenbefore_map [Int]
ps Map Int Bool
sublabel ([Int]
ls[Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++[Int
p])
            else Map Int Bool
-> [Int] -> Map Int Bool -> [Int] -> ([Int], Map Int Bool)
checkEUprevious Map Int Bool
new_seenbefore_map [Int]
ps Map Int Bool
sublabel [Int]
ls
    | Bool
otherwise = Map Int Bool
-> [Int] -> Map Int Bool -> [Int] -> ([Int], Map Int Bool)
checkEUprevious Map Int Bool
seenbefore_map [Int]
ps Map Int Bool
sublabel [Int]
ls 
    where Just previous_bool :: Bool
previous_bool = Int -> Map Int Bool -> Maybe Bool
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
p Map Int Bool
seenbefore_map
          Just previous_marked :: Bool
previous_marked = Int -> Map Int Bool -> Maybe Bool
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
p Map Int Bool
sublabel

checkCTLauxAU :: (CTL a) -> AutomataInfo (CTL a) -> Automata ->  Map.Map Int Bool -> Map.Map Int Int -> [State] ->  Map.Map Int Bool ->  Map.Map Int Bool 
checkCTLauxAU :: CTL a
-> AutomataInfo (CTL a)
-> Automata
-> Map Int Bool
-> Map Int Int
-> [Int]
-> Map Int Bool
-> Map Int Bool
checkCTLauxAU (AU a :: CTL a
a b :: CTL a
b) info :: AutomataInfo (CTL a)
info tom :: Automata
tom label_map :: Map Int Bool
label_map degree_map :: Map Int Int
degree_map (l :: Int
l:ls :: [Int]
ls) sublabel :: Map Int Bool
sublabel =
    let previous_states :: [Int]
previous_states = Set Int -> [Int]
forall a. Set a -> [a]
toList (Automata -> Int -> Set Int
getIncomingStates Automata
tom Int
l)
        f :: p -> Maybe Bool
f _ = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
        new_map :: Map Int Bool
new_map = (Bool -> Maybe Bool) -> Int -> Map Int Bool -> Map Int Bool
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update Bool -> Maybe Bool
forall p. p -> Maybe Bool
f Int
l Map Int Bool
label_map
        (added_previous :: [Int]
added_previous,new_degree_map :: Map Int Int
new_degree_map) = Map Int Bool
-> Map Int Int
-> [Int]
-> Map Int Bool
-> [Int]
-> ([Int], Map Int Int)
checkAUprevious Map Int Bool
new_map Map Int Int
degree_map [Int]
previous_states Map Int Bool
sublabel [Int]
ls
    in CTL a
-> AutomataInfo (CTL a)
-> Automata
-> Map Int Bool
-> Map Int Int
-> [Int]
-> Map Int Bool
-> Map Int Bool
forall a.
CTL a
-> AutomataInfo (CTL a)
-> Automata
-> Map Int Bool
-> Map Int Int
-> [Int]
-> Map Int Bool
-> Map Int Bool
checkCTLauxAU (CTL a -> CTL a -> CTL a
forall a. CTL a -> CTL a -> CTL a
AU CTL a
a CTL a
b) AutomataInfo (CTL a)
info Automata
tom Map Int Bool
new_map Map Int Int
new_degree_map [Int]
added_previous Map Int Bool
sublabel


        
checkAUprevious :: Map.Map Int Bool -> Map.Map Int Int -> [State] -> Map.Map Int Bool -> [State] -> ([State], Map.Map Int Int)
checkAUprevious :: Map Int Bool
-> Map Int Int
-> [Int]
-> Map Int Bool
-> [Int]
-> ([Int], Map Int Int)
checkAUprevious label_map :: Map Int Bool
label_map degree_map :: Map Int Int
degree_map [] sublabel :: Map Int Bool
sublabel ls :: [Int]
ls = ([Int]
ls,Map Int Int
degree_map)
checkAUprevious label_map :: Map Int Bool
label_map degree_map :: Map Int Int
degree_map (p :: Int
p:ps :: [Int]
ps) sublabel :: Map Int Bool
sublabel ls :: [Int]
ls =
    if (Int
new_degree Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0) Bool -> Bool -> Bool
&& (Bool
previous_marked Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
True) Bool -> Bool -> Bool
&& (Bool
label Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
False)
    then Map Int Bool
-> Map Int Int
-> [Int]
-> Map Int Bool
-> [Int]
-> ([Int], Map Int Int)
checkAUprevious Map Int Bool
label_map Map Int Int
new_degree_map [Int]
ps Map Int Bool
sublabel ([Int]
ls[Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++[Int
p])
    else Map Int Bool
-> Map Int Int
-> [Int]
-> Map Int Bool
-> [Int]
-> ([Int], Map Int Int)
checkAUprevious Map Int Bool
label_map Map Int Int
new_degree_map [Int]
ps Map Int Bool
sublabel [Int]
ls
    where Just previous_degree :: Int
previous_degree = Int -> Map Int Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
p Map Int Int
degree_map
          new_degree :: Int
new_degree = Int
previous_degree Int -> Int -> Int
forall a. Num a => a -> a -> a
-1
          f :: p -> Maybe Int
f _ = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
new_degree
          new_degree_map :: Map Int Int
new_degree_map = (Int -> Maybe Int) -> Int -> Map Int Int -> Map Int Int
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update Int -> Maybe Int
forall p. p -> Maybe Int
f Int
p Map Int Int
degree_map
          Just previous_marked :: Bool
previous_marked = Int -> Map Int Bool -> Maybe Bool
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
p Map Int Bool
sublabel
          Just label :: Bool
label = Int -> Map Int Bool -> Maybe Bool
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
p Map Int Bool
label_map