packages feed

FSM (empty) → 1.0.0

raw patch · 8 files changed

+942/−0 lines, 8 filesdep +basedep +containersdep +matrixsetup-changed

Dependencies added: base, containers, matrix, vector

Files

+ ChangeLog.md view
@@ -0,0 +1,3 @@+# Changelog for my-fsm-stack-package++## Unreleased changes
+ FSM.cabal view
@@ -0,0 +1,44 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.31.2.+--+-- see: https://github.com/sol/hpack+--+-- hash: fe188947cbf6cfabbd09d7ce88601c5e5e53a462619fa621cd19b37804881f19++name:           FSM+version:        1.0.0+synopsis:       Basic concepts of finite state machines.+description:    Please see the README on GitHub at <https://github.com/Pablo-Dominguez/my-stack-fsm-package#readme>+category:       FSM+homepage:       https://github.com/Pablo-Dominguez/my-stack-fsm-package#readme+bug-reports:    https://github.com/Pablo-Dominguez/my-stack-fsm-package/issues+author:         Pablo Dominguez+maintainer:     pabdombal@alum.us.es+copyright:      2020 Pablo Dominguez+license:        BSD3+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+    ChangeLog.md++source-repository head+  type: git+  location: https://github.com/Pablo-Dominguez/my-stack-fsm-package++library+  other-modules:+      Paths_FSM+  hs-source-dirs:+      src+  build-depends:+      base >=4.13 && <5+    , containers >=0.5+    , matrix >=0.3.6 && <0.4+    , vector >=0.12.1 && <0.13+  default-language: Haskell2010+  exposed-modules:+    FSM.Automata+    FSM.States+    FSM.Logic
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Author name here (c) 2020++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Author name here nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,17 @@+# A haskell package in model checking++This is the repo for the package I developed in haskell as the project for my dissertation. The package consists in the following three parts:++### FSM.Automata++In this module, we define the `data Automata` so it is possible to construct an Automata, perform basic operations with it or get information from it.++### FSM.States++In this module we strongly use the [Data Map](http://hackage.haskell.org/package/containers-0.6.2.1/docs/Data-Map-Strict.html) package to store information in the states. Although this module may seem simple, it took a lot of hours of designing.++I decided to keep the packages independents from each other so you can use one without having to use the other. Because of this, it is possible to create an `AutomataInfo` object of an `Automata` that is not even defined.++### FSM.Logic++In this final module, we combine the two previous modules and some functions implemented in them so we can apply the CTL model checking algorithm over the `Automata` and the `AutomataInfo`.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ src/FSM/Automata.hs view
@@ -0,0 +1,371 @@++-- Import packages -----------------------------------------++module FSM.Automata (++    Automata,+    -- * Creating functions+    createAutomata,+    +    -- * Accessing functions+    getStates,+    getAcceptingStates,+    getInitialState,+    getInputs,+    getAssociations,+    getTransitions,+    getOutgoingStates,+    getIncomingStates,+    getDeadlocks,+    getIsolated,+    +    -- * Checking functions+    validInput,+        +    -- * Editing functions+    addState,+    deleteState,+    changeInitialState,+    addAcceptingState+     ++) where++import Data.Set +import qualified Data.List   as L+import qualified Data.Matrix as M+import qualified Data.Vector as V++-- Custom show functions ---------------------------------------++showIntSet :: [Int] -> Int -> String+showIntSet [] 0 = id "{" ++ id "}"+showIntSet [] _ = id "}"+showIntSet (l:ls) 0 = id "{" ++ show l ++ showIntSet ls 1+showIntSet (l:ls) k = id "," ++ show l ++ showIntSet ls k++showCharSet :: [Char] -> Int -> String+showCharSet [] 0 = id "{" ++ id "}"+showCharSet [] _ = id "}"+showCharSet (l:ls) 0 = id "{" ++ show l ++ showCharSet ls 1+showCharSet (l:ls) k = id "," ++ show l ++ showCharSet ls k+    +-- Create data types -----------------------------------------++data Automata = A (Set Int,Set Char,Int,M.Matrix Int,Set Int)+                --deriving Show+                +instance Show Automata where+    show (A (s,i,s0,m,a)) = +        (id "\n" ++ id "Set of states:" ++ id "\n" ++ s' ++ id "\n" ) +++        (id "\n" ++ id "Set of inputs (alphabet):" ++ id "\n"  ++ i' ++ id "\n" ) +++        (id "\n" ++ id "Initial state:" ++ id "\n" ++ show s0 ++ id "\n" ) +++        (id "\n" ++ id "Matrix of associations:" ++ id "\n" ++ show m ++ id "\n" ) +++        (id "\n" ++ id "Set of accepting states:" ++ id "\n" ++ a')+        --(id "\n" ++ id "Current state:" ++ id "\n" ++ show c ++ id "\n") ++ id "\n" +        where s' = showIntSet (toList s) 0+              i' = showCharSet (toList i) 0+              a' = showIntSet (toList a) 0++-- Creating functions -----------------------------------------++-- | This is the main function for creating the Automata abstract data type. By default, the inital state and the current state of the automata are the same.+--+--  Please pay attention to how the object is built. E.g.,+--+-- > createAutomata s i s0 m a+--  where:+--+-- -s is the number of states of the automata.+-- -i is the alphabet the automata accepts.+-- -s0 is the initial state of the automata.+-- -m is the matrix of associations of the automata. (Details here: 'getAssociations')+-- -a is the list of accepting states of the automata.+--+-- More specifically you could+--+-- > import qualified Data.Matrix as M+-- > mat = M.fromLists [[2,0,0,0],[2,1,4,0],[1,4,0,0],[0,0,0,3]]+-- > tom = createAutomata 4 ['a', 'b', 'c', 'd'] 1 mat [4]+++createAutomata :: Int -> String -> Int -> M.Matrix Int -> [Int] -> Automata+createAutomata s i s0 m a+    | s < 1 = +        error "Number of states must be greater than 1"+    | not (member s0 s') =+        error "Not valid initial state"+    | not ((M.nrows m,M.ncols m) == (size s',size i')) =+        error "Not valid matrix size"+    | not (isSubsetOf (delete 0 (fromList (M.toList m))) s') =+        error "Not valid matrix elems"+    | not (isSubsetOf a' s') =+        error "Not valid accepting states"+    | otherwise = A (s',i',s0,m,a')+      where s' = fromList [1..s]+            i' = fromList (L.sort i)+            a' = fromList (L.sort a)++++-- Accessing functions ----------------------------------------- + + +-- | This function returns the set of states of the automata. It is really of not much use since the generation of the automata only needs the number of states and not the whole set of them, but just in case you want to check which states does the current automata have. +getStates :: Automata -> Set Int +getStates t = s+    where A (s,i,s0,m,a) = t++-- | This function returns the list of accepting states of the automata. It is a list and not a set for coherence purpouses. When you build the automata you have to give a list of accepting states so I though it made sense to also return a list of accepting states as the accessing function.+getAcceptingStates :: Automata -> [Int]+getAcceptingStates t = a'+    where A (s,i,s0,m,a) = t     +          a' = toList a++-- | This function returns the current initial state of the automata.+getInitialState :: Automata -> Int +getInitialState t = s0+    where A (s,i,s0,m,a) = t ++-- | This function returns the string of inputs (alphabet) that the automata accepts.    +getInputs :: Automata -> String+getInputs t = toList i+    where A (s,i,s0,m,a) = t +          +-- | This function returns the associations matrix of the automata.  This matrix is built according to the following rules:+--+-- 1. The columns of the matrix represent the inputs of the alphabet that the automata accepts in <https://en.wikipedia.org/wiki/Lexicographical_order lexicographical order>.+-- 2. The rows of the matrix represent the states of the automata in ascending order.+-- 3. The element \(a_{ij} = k \) means that the state  \(i\) is connected to the state  \(k\) thanks to the input that the column  \(j\)  of the matrix represents.+--+-- More info can be found here: <https://en.wikipedia.org/wiki/State-transition_table Wikipedia: State-transition table>+--+-- Continuing with the previous example, the following matrix correspongs to the automata in the figure.+--+-- > mat = M.fromLists [[2,0,0,0],[2,1,4,0],[1,4,0,0],[0,0,0,3]]+-- > tom = createAutomata 4 ['a', 'b', 'c', 'd'] 1 mat [4] 1+--+-- The code above represent this matrix: +--+-- >     'a' 'b' 'c' 'd'         <= inputs+-- >   ------------------+-- > 1 |  2   0   0   0 +-- > 2 |  2   1   4   0  +-- > 3 |  1   4   0   0 +-- > 4 |  0   0   0   3  +-- > +-- > ^+-- > |+-- > states+-- +-- And the matrix above represents the transitions in the following automata:+--+-- <<https://i.imgur.com/ymWLlsb.png Tom automata figure>>+{-+--+-- +-----------+------------+----------+----------+----------++-- |           | 'a'        | 'b'      | 'c'      | 'd'      |  +-- +-----------+------------+----------+----------+----------++-- | 1         |  \[                                         |+-- +-----------+    \begin{matrix}                           |+-- | 2         |                                             |+-- +-----------+                                             |+-- | 3         |                                             |+-- +-----------+                                             |+-- | 4         |    2 & 0 & 0 & 0 \\                         |+-- |           |    2 & 1 & 4 & 0 \\                         |+-- |           |    1 & 4 & 0 & 0 \\                         |+-- |           |    0 & 0 & 0 & 3                            |+-- |           |    \end{matrix}                             |+-- |           |                                             |+-- |           |    \]                                       |+-- +-----------+------------+----------+----------+----------++--+-}++getAssociations :: Automata -> M.Matrix Int+getAssociations t = m+    where A (s,i,s0,m,a) = t+         +-- | This function returns the inputs that a state accepts for transitioning into another state.+--+getTransitions :: Automata -> Int -> Set Char+getTransitions t k +    | not (member k s) = error "Not a valid state"+    | otherwise = fromList l+    where m = getAssociations t+          i = getInputs t+          s = getStates t+          row = V.toList (M.getRow k m)+          l = [ a | (a,k) <- zip i row, k /= 0]+          ++-- -- | This function returns the current state in which the automata currently is.+-- --+-- getCurrentState :: Automata -> Int+-- getCurrentState t = c+--     where A (s,i,s0,m,a,c) = t +          +-- | This function returns the states you can possibly reach from a given state.+--+getOutgoingStates :: Automata -> Int -> Set Int+getOutgoingStates t k+    | not (member k s) = error "Not a valid state"+    | otherwise = fromList l+    where m = getAssociations t+          s = getStates t+          row = V.toList (M.getRow k m)+          l = [ p | p <- row, p /= 0]+          +-- | This function returns the states that can possibly reach a given state.+--+getIncomingStates :: Automata -> Int -> Set Int+getIncomingStates t k+    | not (member k s) = error "Not a valid state"+    | otherwise = fromList l+    where m = getAssociations t+          s = getStates t+          rows = [(n,member k (fromList (V.toList (M.getRow n m)))) | n <- [1..(M.nrows m)]]+          l = [n | (n,bool) <- rows, bool == True]         +          +-- | This function returns those states of the automata that do not have any input to any other state (except for itself), i.e., once that a 'deadlock' state is reached, none of the rest of state can be reached anymore for the current execution.+getDeadlocks :: Automata -> Set Int+getDeadlocks t = Data.Set.filter (\ p -> (Data.Set.null (getOutgoingStates t p) || +                                        (getOutgoingStates t p) == Data.Set.fromList [p])) s+    where A (s,i,s0,m,a) = t +-- getDeadlocks :: Automata -> Set Int+-- getDeadlocks t = fromList hs+--     where A (s,i,s0,m,a,c) = t +--           hs = [n | n <- toList s,+--                 and [n == (M.getRow n m)V.!k || (M.getRow n m)V.!k == 0 | k <- [0..((size i)-1)]]]++-- | This function returns the states of the given automata that cannot be reached.+--+getIsolated :: Automata -> Set Int+getIsolated t = Data.Set.filter (\ p -> (Data.Set.null (getIncomingStates t p) ||+                                (getIncomingStates t p) == Data.Set.fromList [p])) s+  where A (s,i,s0,m,a) = t+{-+getIsolated :: Automata -> Set Int+getIsolated t = fromList l+    where s = getStates t+          l = [ p | p <- toList s, getIncomingStates t p == empty]-}+++-- Checking functions -----------------------------------------++validInputAux :: String -> Automata -> Int -> Bool+validInputAux str a k+    | not (isSubsetOf (fromList str) i) = error "Invalid input"+    | L.null str = member k ac+    | not (member st (getTransitions a k)) =  error ("Not valid input "  ++ (show st) ++ " for state " ++ (show k) )+    | otherwise = validInputAux (tail str) a k'+    where s = getStates a+          i = fromList (getInputs a)+          s0 = getInitialState a+          m = getAssociations a+          ac = fromList (getAcceptingStates a)+          st = head str+          k' = M.getElem k ((findIndex st i)+1) m+         ++++-- | This function test if a string is @/valid/@, i.e., if when the automata receives the string, ends in one of the accepting states.+validInput :: String -> Automata -> Bool+validInput str a = validInputAux str a s0+    where s0 = getInitialState a++-- -- Action functions+-- +-- -- | This funcion perform the given transition from the current state and changes to a new current state.+-- performAction :: Automata -> Char -> Automata+-- performAction t char+--     | not (member char i) = error ("This is not one of the valid inputs. Please try again with one of the following options: " ++ ts')+--     | not (member char ts) = error ("This is not one of the valid inputs for the current state. Please try again with one of the following options: " ++ ts')+--     | otherwise = changeCurrentState t c'+--         where i = fromList (getInputs t)+--               c = getCurrentState t+--               ts = getTransitions t c+--               ts' = showCharSet (toList ts) 0+--               m = getAssociations t+--               n = (findIndex char i) + 1+--               c' = M.getElem c n m++-- Editing functions -----------------------------------------+++-- | Function for adding a state to an Automata with the list of associations to the other states. If you would want to add a non-connected state, simply enter the list [0,..,0], with as many zeros as possible inputs. +addState :: Automata -> [Int] -> Automata+addState a ls +    | L.length ls /= L.length (getInputs a) = error ( "Not a valid list of associations" ) +    | otherwise = createAutomata s i s0 m t+    where s = (M.nrows (getAssociations a)) +1+          i = getInputs a+          s0 = getInitialState a+          t = getAcceptingStates a+          m = M.fromLists ((M.toLists (getAssociations a))++[ls])++dropElemAtIndex :: Int -> [[Int]] -> [[Int]]+dropElemAtIndex i ls = L.take (i-1) ls ++ L.drop i ls++-- | This function deletes a state and all the connections it has with any other state. Please note that this function automatically reassigns new numbers for the remaining states, so the states and the associations matrix change accordingly. E.g. if you delete in the previous automata the 3rd state, then since the new automata has just 3 states, the old 4th state becomes the new 3rd state.+deleteState :: Automata -> Int ->Automata+deleteState a i +    | not (elem i (getStates a)) = a+        --error ( "This state is not one of the states of the automata." )+    | (getInitialState a) == i = error ( "You are trying to delete the initial state. If you want to perform this action, first change the initial state and then delete the old one.")+    | elem i (fromList (getAcceptingStates a)) && L.length (getAcceptingStates a) == 1 = error ("You are trying to delete the only accepting state.")+    | otherwise = createAutomata s i' s0' m t+    where s = (M.nrows (getAssociations a)) -1+          i' = getInputs a+          s0 = getInitialState a+          s0' = if s0 < i then s0 else s0-1+          t = [if l < i then l else l-1 | l <- toList ((fromList (getAcceptingStates a)) `difference` singleton i)]+          rows = M.toLists (getAssociations a)+          rows_deleted = dropElemAtIndex i ([[if l < i +                                              then l+                                              else if l > i+                                                   then l-1+                                                   else 0 | l <- ls] | ls <- rows])+          m = M.fromLists rows_deleted++-- | This function changes the initial state.+changeInitialState :: Automata -> Int -> Automata+changeInitialState t s0' +    | not (elem s0' (getStates t)) = error ( "This state is not one of the states of the automata." )+    | (getInitialState t) == s0' = error ( "State " ++ show s0' ++ " is already the initial state.")+    | otherwise = createAutomata s' i' s0' m a+        where a = getAcceptingStates t +              s' = size (getStates t)+              i' = getInputs t+              m = getAssociations t++-- -- | This function changes the current state.+-- changeCurrentState :: Automata -> Int -> Automata+-- changeCurrentState t c'+--     | not (elem c' (getStates t)) = error ( "This state is not one of the states of the automata." )+--     | (getCurrentState t) == c' = error ( "State " ++ show c' ++ " is already the current state.")+--     | otherwise = createAutomata s' i' s0 m a c+--         where a = getAcceptingStates t +--               s0 = getInitialState t+--               c = getCurrentState t+--               s' = size (getStates t)+--               i' = getInputs t+--               m = getAssociations t +    +-- | This function adds one accepting state+--+addAcceptingState :: Automata -> Int -> Automata+addAcceptingState t a0+    | not (elem a0 (getStates t)) = error ( "This state is not one of the states of the automata." )+    | elem a0 (getAcceptingStates t)  = error ( "State " ++ show a0 ++ " is already one of the accepting states.")+    | otherwise = createAutomata s' i' s0 m a'+    where a = getAcceptingStates t+          a' = a ++ [a0]+          s' = size (getStates t)+          i' = getInputs t+          m = getAssociations t+          s0 = getInitialState t+          +
+ src/FSM/Logic.hs view
@@ -0,0 +1,246 @@++module FSM.Logic (+    -- * Definition of the CTL language+    CTL (..),+    +    -- * Implementation of the model checking algorithm for CTL+    checkCTL,+    modelsCTL,+    checkFormulas++) 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 = CTrue | CFalse -- ^ Basic bools.+        | RArrow (CTL a) (CTL a) -- ^ Basic imply.+        | DArrow (CTL a) (CTL a) -- ^ Basic double imply.+        | 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 (Ord,Show)++instance Eq a => Eq (CTL a) where+    (CTrue) == Not (CFalse) = True+    (Atom a) == (Atom b) = a == b+    (Not a) == (Not b) = a == b+    (And a b) == (And c d) = (a == c) && (b == d)+    (Or a b) == (Or c d) = (a == c) && (b == d)+    (RArrow a b) == (Or (Not c) d) = (a == c) && (b == d)+    (EX a) == (EX b) = a == b+    (EF a) == (EF b) = a == b+    (EG a) == (EG b) = a == b+    (AX a) == (AX b) = a == b+    (AF a) == (AF b) = a == b+    (AG a) == (AG b) = a == b+    (EU a b) == (EU c d) = (a == c) && (b == d)+    (AU a b) == (AU c d) = (a == c) && (b == d)+    -- Aditional equivalences+    (Or a b) == (Not (And (Not c) (Not d))) = (a == c) && (b == d)+    (And a b) == (Not (Or (Not c) (Not d))) = (a == c) && (b == d)+    Not (Not a) == b = a == b+    +    (AX a) == (Not (EX (Not b))) = a == b+    (AF a) == (Not (EX (Not b))) = a == b+    (AG a) == (Not (EX (Not b))) = a == b+    +    (EX a) == (Not (AX (Not b))) = a == b+    (EF a) == (Not (AX (Not b))) = a == b+    (EG a) == (Not (AX (Not b))) = a == b+    +    (AU a b) == Not (Or (EU (Not c1) (Not (Or d c2))) (EG (Not c3))) = (a == d) && (b == c1) && (c1 == c2) && (c2 == c3)++data LTL a = LTL_Atom a -- ^ It defines an atomic statement. E.g.:     'Atom' @"The plants look great."@+        | LTL_Not (LTL a) --  'Not' negates a 'CTL' formula.+        | LTL_And (LTL a) (LTL a) --  'And' +        | LTL_Or (LTL a) (LTL a)+        | LTL_X (LTL a) -- ^ 'EX' means that the 'CTL' formula holds in at least one of the inmediate successors states.+        | LTL_F (LTL a) -- ^ 'EF' means that the 'CTL' formula holds in at least one of the future states.+        | LTL_G (LTL a) -- ^ 'EG' means that the 'CTL' formula holds always from one of the future states.+        | LTL_U (LTL a) (LTL 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.+        deriving (Ord,Show)   +        +instance Eq a => Eq (LTL a) where+    (LTL_Atom a) == (LTL_Atom b) = a == b+    (LTL_Not a) == (LTL_Not b) = a == b+    (LTL_And a b) == (LTL_And c d) = (a == c) && (b == d)+    (LTL_Or a b) == (LTL_Or c d) = (a == c) && (b == d)+    (LTL_X a) == (LTL_X b) = a == b+    (LTL_F a) == (LTL_F b) = a == b+    (LTL_G a) == (LTL_G b) = a == b+    (LTL_U a b) == (LTL_U c d) = (a == c) && (b == d)+    -- Aditional equivalences+    (LTL_Or a b) == (LTL_Not (LTL_And (LTL_Not c) (LTL_Not d))) = (a == c) && (b == d)+    (LTL_And a b) == (LTL_Not (LTL_Or (LTL_Not c) (LTL_Not d))) = (a == c) && (b == d)+    +++-- | 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 CTrue tom info = +    let states = (toList (getStates tom))+    in Map.fromList [(x,True) | x <- states]+checkCTL (Atom a) tom info =+    let states = (toList (getStates tom))+    in checkCTLauxAtom (Atom a) info tom states Map.empty+checkCTL (Not a) tom info = checkCTLauxNot (checkCTL a tom info)+checkCTL (And a b) tom info = checkCTLauxAnd (checkCTL a tom info) (checkCTL b tom info)+checkCTL (Or a b) tom info = checkCTL (Not (And (Not a) (Not b))) tom info+checkCTL (RArrow a b) tom info = checkCTL (Or (Not a) b) tom info+checkCTL (DArrow a b) tom info = checkCTL (Or (And a b) (And (Not a) (Not b))) tom info+checkCTL (EX a) tom info =+  let states = (toList (getStates tom))+      sublabel = checkCTL a tom info+  in checkCTLauxEX tom states sublabel (Map.fromList [(x,False) | x <- states])+checkCTL (AX a) tom info = checkCTL (Not (EX (Not a))) tom info+checkCTL (EU a b) tom info = +    let sublabel1 = checkCTL a tom info+        sublabel2 = checkCTL b tom info+        states = (toList (getStates tom))+        init_list = [x | (x,k) <- (Map.toList sublabel2), k == True]+    in checkCTLauxEU tom (Map.fromList [(x,False) | x <- states]) (Map.fromList [(x,False) | x <- states]) init_list sublabel1+checkCTL (EF a) tom info = checkCTL (EU CTrue a) tom info+checkCTL (AU a b) tom info = +    let sublabel1 = checkCTL a tom info+        sublabel2 = checkCTL b tom info+        states = (toList (getStates tom))+        degree_map = Map.fromList [(x,length (toList (getOutgoingStates tom x))) | x <- states]+        label_map = (Map.fromList [(x,False) | x <- states])+        init_list = [x | (x,k) <- (Map.toList sublabel2), k == True]+    in checkCTLauxAU tom label_map degree_map init_list sublabel1+checkCTL (AF a) tom info = checkCTL (AU CTrue a) tom info+checkCTL (EG a) tom info = checkCTL (Not (AF (Not a))) tom info+checkCTL (AG a) tom info = checkCTL (Not (EF (Not a))) tom info+    ++checkCTLauxAtom :: Eq a => CTL a -> AutomataInfo (CTL a) -> Automata -> [State] ->  Map.Map Int Bool -> Map.Map Int Bool+checkCTLauxAtom (Atom a) info tom [] label_map = label_map+checkCTLauxAtom (Atom a) info tom (l:ls) label_map =+  let content_info = getStateInfo (getInfoInState info l Nothing) +      content = Map.elems content_info+      new_bool = elem (Atom a) content+      f _ = Just new_bool+      new_map = Map.alter f l label_map+  in checkCTLauxAtom (Atom a) info tom ls new_map   +    +    +checkCTLauxNot :: Map.Map Int Bool -> Map.Map Int Bool+checkCTLauxNot label_map = notMapAux label_map (Map.keys label_map)++notMapAux :: Map.Map Int Bool -> [Int] -> Map.Map Int Bool+notMapAux label_map [] = label_map+notMapAux label_map (l:ls) = +    let Just old_bool = Map.lookup l label_map+        f _ = Just (not old_bool)+        new_map = Map.update f l label_map+    in notMapAux new_map ls+            +checkCTLauxAnd :: Map.Map Int Bool -> Map.Map Int Bool -> Map.Map Int Bool+checkCTLauxAnd label_map1 label_map2 = andMapAux label_map1 label_map2 (Map.keys label_map1)++andMapAux ::  Map.Map Int Bool -> Map.Map Int Bool -> [Int] -> Map.Map Int Bool+andMapAux label_map1 label_map2 [] = label_map1+andMapAux label_map1 label_map2 (l:ls) =+    let Just bool1 = Map.lookup l label_map1+        Just bool2 = Map.lookup l label_map2+        f _ = Just (bool1 && bool2)+        new_map = Map.update f l label_map1+    in andMapAux new_map label_map2 ls+    +checkCTLauxEX :: Automata -> [State] ->  Map.Map Int Bool -> Map.Map Int Bool -> Map.Map Int Bool+checkCTLauxEX tom [] label_map marked_map = marked_map+checkCTLauxEX tom (l:ls) label_map marked_map =+    let connected = toList (getOutgoingStates tom l)+        connected_map = Map.filterWithKey (\k _ -> (elem k connected)) label_map+        new_bool = or (Map.elems connected_map)+        f _ = Just new_bool+        new_map = Map.update f l marked_map -- es alter?+    in checkCTLauxEX tom ls label_map new_map++checkCTLauxEU :: Automata ->  Map.Map Int Bool -> Map.Map Int Bool -> [State] -> Map.Map Int Bool -> Map.Map Int Bool+checkCTLauxEU tom label_map seenbefore_map [] sublabel = label_map+checkCTLauxEU tom label_map seenbefore_map (k:ks) sublabel = +    let previous_states = toList (getIncomingStates tom k)+        f _ = Just True+        new_map = Map.update f k label_map+        (added_previous,new_seenbefore_map) = checkEUprevious seenbefore_map previous_states sublabel ks+    in checkCTLauxEU tom new_map new_seenbefore_map added_previous sublabel+        +        +checkEUprevious :: Map.Map Int Bool -> [State] -> Map.Map Int Bool -> [State] -> ([State],Map.Map Int Bool)+checkEUprevious seenbefore_map [] sublabel ls = (ls,seenbefore_map)+checkEUprevious seenbefore_map (p:ps) sublabel ls +    | previous_bool == False = +        let f _ = Just True+            new_seenbefore_map = Map.update f p seenbefore_map+        in if previous_marked == True+            then checkEUprevious new_seenbefore_map ps sublabel (toList (fromList (ls++[p])))+            else checkEUprevious new_seenbefore_map ps sublabel ls+    | otherwise = checkEUprevious seenbefore_map ps sublabel ls +    where Just previous_bool = Map.lookup p seenbefore_map+          Just previous_marked = Map.lookup p sublabel++checkCTLauxAU :: Automata ->  Map.Map Int Bool -> Map.Map Int Int -> [State] ->  Map.Map Int Bool ->  Map.Map Int Bool +checkCTLauxAU tom label_map degree_map [] sublabel = label_map+checkCTLauxAU tom label_map degree_map (l:ls) sublabel =+    let previous_states = toList (getIncomingStates tom l)+        f _ = Just True+        new_map = Map.update f l label_map+        (added_previous,new_degree_map) = checkAUprevious new_map degree_map previous_states sublabel ls+    in checkCTLauxAU tom new_map new_degree_map added_previous sublabel+        +checkAUprevious :: Map.Map Int Bool -> Map.Map Int Int -> [State] -> Map.Map Int Bool -> [State] -> ([State], Map.Map Int Int)+checkAUprevious label_map degree_map [] sublabel ls = (ls,degree_map)+checkAUprevious label_map degree_map (p:ps) sublabel ls =+    if (new_degree == 0) && (previous_marked == True) && (label == False)+    then checkAUprevious label_map new_degree_map ps sublabel (toList (fromList (ls++[p])))+    else checkAUprevious label_map new_degree_map ps sublabel ls+    where Just previous_degree = Map.lookup p degree_map+          new_degree = previous_degree -1+          f _ = Just new_degree+          new_degree_map = Map.update f p degree_map+          Just previous_marked = Map.lookup p sublabel+          Just label = Map.lookup p label_map++-- | This function returns the result of \(automata \models formula \).+--          +modelsCTL :: Eq a => CTL a -> Automata -> AutomataInfo (CTL a) -> Bool+modelsCTL a tom info = model+    where (Just model) = Map.lookup (getInitialState tom) (checkCTL a tom info)+          ++          +-- | This function loops over multiple formulas and tells you if the automata models each formula.+--+checkFormulas :: Eq a => Automata -> AutomataInfo (CTL a) -> [CTL a] -> [Bool] -> [Bool]+checkFormulas tom info [] bs = bs+checkFormulas tom info (l:ls) bs = checkFormulas tom info ls (bs++[modelsCTL l tom info])
+ src/FSM/States.hs view
@@ -0,0 +1,229 @@++-- |+--+-- = Considerations+--+-- One caveat you should always take into account when using this package is that without some data creation from the user, the use of this package is a bit restricted. This happens because the way it is built the package forbids you to use more than one type of information between states (or inside one), so to work around this, if you want to have multiple types of information inside states, do as follows:+--+-- @+--   data CustomData = Type1 String | Type2 Int deriving (Show,Eq)+-- @+-- +-- dont forget about the deriving because otherwise it will conflict with the functions in the package.+  +++module FSM.States (+    State,+    Tag,+    StateInfo,+    AutomataInfo,+        +    -- * Creating functions+    createStateInfo,+    fromlsStateInfo,+        +    -- * Accessing functions+    getStateInfo,+    getStatesWithInfo,+    getTagsInState,+    getInfoInState,+    +    -- * Editing functions+    alterStateInfo,+    unionStateInfo+    ++) where++import qualified Data.Map as Map   +import qualified Data.List as L++type State = Int+type Tag = String+++newtype StateInfo a = StateInfo {tagMap :: Map.Map Tag a} deriving Eq+newtype AutomataInfo a = AutomataInfo { toMap :: Map.Map State (StateInfo a)} deriving Eq++--data UserStateInfo = UserStateInfo { rate :: Float } deriving Show++verboseShowStateInfo :: Show a => Map.Map Tag a -> String+verboseShowStateInfo = concatMap formatter . Map.toAscList+  where formatter (k, v) = concat ["--> [tag] ",k, ": ","\n", show v, "\n"]+        +instance Show a => Show (StateInfo a) where+  show = verboseShowStateInfo . tagMap        +  +verboseShow :: Show a => Map.Map State (StateInfo a) -> String+verboseShow = concatMap formatter . Map.toAscList+  where formatter (s, i) = concat ["=> The elements in state ", show s, " are:\n", verboseShowStateInfo (tagMap i), "\n"]+++instance Show a => Show (AutomataInfo a) where+  show = verboseShow . toMap ++  +-- Creating functions ------------------------++-- | This function takes a State, a Tag and a value and creates an AutomataInfo object containing only the given State with the value and the tag associated to it.+-- E.g.:+--+-- > createStateInfo 4 "tag" 25+-- +-- If you created your own data type, you can do as follows:+--+-- > my_info = createStateInfo 4 "tag" (Type2 25)+--+createStateInfo :: State -> Tag -> a -> AutomataInfo a+createStateInfo state tag k = AutomataInfo {toMap = Map.singleton state (StateInfo {tagMap = Map.singleton tag k})}++-- | This function takes a State, a list of (Tag,value) and Maybe AutomataInfo and returns the AutomataInfo updated with the list of tags given. Please notice that if Nothing is given, it will return the created AutomataInfo while if a (Just AutomataInfo) object is given, it will update the tags in the given state.+-- E.g. (notice that we are using @my_info@ from the previous example)+--+-- > fromlsStateInfo 4 [("foo", Type1 "on"),("bar", Type2 0)] Nothing+-- > fromlsStateInfo 4 [("foo", Type1 "on"),("bar", Type2 0)] (Just my_info)+--+fromlsStateInfo :: Eq a => State -> [(Tag,a)] -> Maybe (AutomataInfo a) -> AutomataInfo a+fromlsStateInfo state [] Nothing = AutomataInfo {toMap = Map.empty}+fromlsStateInfo state (l:ls) Nothing +    | ls /= [] = fromlsStateInfo state ls (Just first_info)+    | otherwise = first_info+    where (tag,value) = l+          first_info = createStateInfo state tag value+fromlsStateInfo state [] (Just info) = info+fromlsStateInfo state (l:ls) (Just (AutomataInfo info)) +    | ls /= [] = fromlsStateInfo state ls (Just new_aut_info)+    | otherwise = new_aut_info+    where (tag,value) = l+          new_info = createStateInfo state tag value+          new_aut_info = unionStateInfo new_info (AutomataInfo info)+          +{-+-- quiero hacer una funcion que une la info con dos AutomataInfos (unión de conjuntos)+-- y otra funcion que a partir de un (State,[(Tag,a)]) crea el AutomataInfo+fromListAux :: Int -> [(State,[(Tag,a)])] -> AutomataInfo a+fromListAux 0 (l:ls) = +    where (state,tag_list) = l+          +++fromListStateInfo :: [(State,[(Tag,a)])] -> AutomataInfo a+fromListStateInfo ls = fromListAux 0 ls+-}++-- Accessing functions ------------------------++getStateInfo :: StateInfo a -> Map.Map Tag a+getStateInfo (StateInfo k) = k+++-- | This function returns the states of the given AutomataInfo that currently contain some information+--+getStatesWithInfo :: AutomataInfo a -> [State]+getStatesWithInfo (AutomataInfo k) = Map.keys k++-- | This function returns the tags that a given state contains inside the AutomataInfo+--+getTagsInState :: AutomataInfo a -> State -> [Tag]+getTagsInState (AutomataInfo k) n+    | not (elem n (getStatesWithInfo (AutomataInfo k))) =  error ("This state does not contain info.")+    | otherwise = Map.keys (tagMap state_map)+    where (Just state_map) = Map.lookup n k+++-- | This function returns the information contained in the given state. If @Nothing@ is given, then it returns all the information in the state while if @Just tag@ is given, it will return only the information inside the given tag.+-- E.g:+-- +-- > getInfoInState my_info 4 Nothing+-- > getInfoInState my_info 4 (Just "foo")+--+getInfoInState :: AutomataInfo a -> State -> (Maybe Tag) -> StateInfo a+getInfoInState (AutomataInfo k) n Nothing+    | not (elem n (getStatesWithInfo (AutomataInfo k))) = StateInfo Map.empty+        --error ("This state does not contain info.")+    | otherwise = state_map+    where (Just state_map) = Map.lookup n k+getInfoInState (AutomataInfo k) n (Just tag)+    | not (elem n (getStatesWithInfo (AutomataInfo k))) = StateInfo Map.empty+       -- error ("This state does not contain info.")+    | not (elem tag (getTagsInState (AutomataInfo k) n)) = StateInfo Map.empty+        --error ("This state does not contain the given tag.")+    | otherwise = output+    where (Just state_map) = Map.lookup n k+          tag_map = tagMap state_map+          Just tag_info = Map.lookup tag tag_map+          output = StateInfo {tagMap = Map.singleton tag tag_info}++-- Editing functions ---------------++-- | This function takes a State, Maybe Tag, a value and an AutomataInfo object and updates the value of the Tag in the given State. Please note that if if Nothing is given, it will delete the State.+-- E.g:+--+-- > alterStateInfo 3 (Just "foo") (Type2 45) my_info+--+alterStateInfo :: State -> Maybe Tag -> a -> AutomataInfo a -> AutomataInfo a+alterStateInfo state Nothing _ (AutomataInfo info)+    | not (elem state (getStatesWithInfo (AutomataInfo info))) = (AutomataInfo info)+        --error ("This state does not contain info.")+    | otherwise = AutomataInfo {toMap = Map.delete state info}+alterStateInfo state (Just tag) sinf (AutomataInfo info) +    | elem state (getStatesWithInfo (AutomataInfo info)) = +        let f _ = Just sinf+            (Just state_map) = Map.lookup state info+            tag_map = tagMap state_map+            new_tag_map = Map.alter f tag tag_map+            g _ = Just (StateInfo {tagMap = new_tag_map})+            new_state_map = Map.alter g state info+        in AutomataInfo {toMap = new_state_map}+    | otherwise = +        let new_tag_map = StateInfo {tagMap = Map.singleton tag sinf}+            g _ = Just new_tag_map+            new_state_map = Map.alter g state info+        in AutomataInfo {toMap = new_state_map}++{-+emptyState :: State -> AutomataInfo a+emptyState state = AutomataInfo {toMap = Map.singleton state output}+        where output = StateInfo {tagMap = Map.empty}-}++-- unionStateAux :: AutomataInfo a -> AutomataInfo a -> AutomataInfo a -> [State] -> AutomataInfo a+-- unionStateAux (AutomataInfo info1) (AutomataInfo info2) (AutomataInfo output) [l] +--     | (elem l (getStatesWithInfo (AutomataInfo info1))) && (not (elem l (getStatesWithInfo (AutomataInfo info2)))) = (AutomataInfo output)+--     | (not (elem l (getStatesWithInfo (AutomataInfo info1)))) && (elem l (getStatesWithInfo (AutomataInfo info2))) = +--         let tag_map2 = tagMap (getInfoInState (AutomataInfo info2) l Nothing)+--             tag_output = StateInfo {tagMap = tag_map2}+--             state_output = Map.singleton l tag_output+--         in (AutomataInfo (Map.union state_output output))+--     | otherwise = +--         let tag_map1 = tagMap (getInfoInState (AutomataInfo info1) l Nothing)+--             tag_map2 = tagMap (getInfoInState (AutomataInfo info2) l Nothing)+--             tag_output = StateInfo {tagMap = Map.union tag_map1 tag_map2}+--             state_output = Map.singleton l tag_output+--         in (AutomataInfo (Map.union state_output output))+unionStateAux (AutomataInfo info1) (AutomataInfo info2) (AutomataInfo output) [] = (AutomataInfo output)+unionStateAux (AutomataInfo info1) (AutomataInfo info2) (AutomataInfo output) (l:ls)+    | (elem l (getStatesWithInfo (AutomataInfo info1))) && (not (elem l (getStatesWithInfo (AutomataInfo info2)))) = unionStateAux (AutomataInfo info1) (AutomataInfo info2) (AutomataInfo output) ls+    | (not (elem l (getStatesWithInfo (AutomataInfo info1)))) && (elem l (getStatesWithInfo (AutomataInfo info2))) = +        let tag_map2 = tagMap (getInfoInState (AutomataInfo info2) l Nothing)+            tag_output = StateInfo {tagMap = tag_map2}+            state_output = Map.singleton l tag_output+        in unionStateAux (AutomataInfo info1) (AutomataInfo info2) (AutomataInfo (Map.union state_output output)) ls+    | otherwise = +        let tag_map1 = tagMap (getInfoInState (AutomataInfo info1) l Nothing)+            tag_map2 = tagMap (getInfoInState (AutomataInfo info2) l Nothing)+            tag_output = StateInfo {tagMap = Map.union tag_map1 tag_map2}+            state_output = Map.singleton l tag_output+        in unionStateAux (AutomataInfo info1) (AutomataInfo info2) (AutomataInfo (Map.union state_output output)) ls+            +-- | This function takes the left-biased union of t1 and t2. It prefers t1 when duplicate keys are encountered. Works similarly to <http://hackage.haskell.org/package/containers-0.6.2.1/docs/Data-Map-Strict.html#g:12 Data.Map.union>.+--+{-unionStateInfo :: AutomataInfo a -> AutomataInfo a -> AutomataInfo a+unionStateInfo (AutomataInfo info1) (AutomataInfo info2) = unionStateAux (AutomataInfo info1) (AutomataInfo info2) (AutomataInfo info1) ls+    where ls = L.union (getStatesWithInfo (AutomataInfo info1)) (getStatesWithInfo (AutomataInfo info2))-} +          +unionStateInfo :: AutomataInfo a -> AutomataInfo a -> AutomataInfo a+unionStateInfo (AutomataInfo info1) (AutomataInfo info2) =+  AutomataInfo (Map.unionWith (\ (StateInfo sti1) (StateInfo sti2) ->+                                 (StateInfo (Map.union sti1 sti2)))+                info1 info2)