-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Basic concepts of finite state machines.
--
-- Please see the README on GitHub at
-- https://github.com/Pablo-Dominguez/my-stack-fsm-package#readme
@package FSM
@version 1.0.0
module FSM.Automata
data Automata
-- | 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 -> Matrix Int -> [Int] -> Automata
-- | 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
-- | 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]
-- | This function returns the current initial state of the automata.
getInitialState :: Automata -> Int
-- | This function returns the string of inputs (alphabet) that the
-- automata accepts.
getInputs :: Automata -> String
-- | This function returns the associations matrix of the automata. This
-- matrix is built according to the following rules:
--
--
-- - The columns of the matrix represent the inputs of the alphabet
-- that the automata accepts in lexicographical order.
-- - The rows of the matrix represent the states of the automata in
-- ascending order.
-- - The element <math> means that the state <math> is
-- connected to the state <math> thanks to the input that the
-- column <math> of the matrix represents.
--
--
-- More info can be found here: 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:
--
getAssociations :: Automata -> Matrix Int
-- | This function returns the inputs that a state accepts for
-- transitioning into another state.
getTransitions :: Automata -> Int -> Set Char
-- | This function returns the states you can possibly reach from a given
-- state.
getOutgoingStates :: Automata -> Int -> Set Int
-- | This function returns the states that can possibly reach a given
-- state.
getIncomingStates :: Automata -> Int -> Set Int
-- | 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
-- | This function returns the states of the given automata that cannot be
-- reached.
getIsolated :: Automata -> Set Int
-- | 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
-- | 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
-- | 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
-- | This function changes the initial state.
changeInitialState :: Automata -> Int -> Automata
-- | This function adds one accepting state
addAcceptingState :: Automata -> Int -> Automata
instance GHC.Show.Show FSM.Automata.Automata
-- | 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
type State = Int
type Tag = String
data StateInfo a
data AutomataInfo a
-- | 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
-- | 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
getStateInfo :: StateInfo a -> Map Tag a
-- | This function returns the states of the given AutomataInfo that
-- currently contain some information
getStatesWithInfo :: AutomataInfo a -> [State]
-- | This function returns the tags that a given state contains inside the
-- AutomataInfo
getTagsInState :: AutomataInfo a -> State -> [Tag]
-- | 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
-- | 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
-- | This function takes the left-biased union of t1 and t2. It prefers t1
-- when duplicate keys are encountered. Works similarly to
-- Data.Map.union.
unionStateInfo :: AutomataInfo a -> AutomataInfo a -> AutomataInfo a
instance GHC.Classes.Eq a => GHC.Classes.Eq (FSM.States.AutomataInfo a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (FSM.States.StateInfo a)
instance GHC.Show.Show a => GHC.Show.Show (FSM.States.AutomataInfo a)
instance GHC.Show.Show a => GHC.Show.Show (FSM.States.StateInfo a)
module FSM.Logic
-- | This is the definition of the CTL language. More info about this
-- language can be found 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.
--
-- Source: A SAFE COTS-BASED DESIGN FLOW OF EMBEDDED SYSTEMS by
-- Salam Hajjar
data CTL a
CTrue :: CTL a
-- | Basic bools.
CFalse :: CTL a
-- | Basic imply.
RArrow :: CTL a -> CTL a -> CTL a
-- | Basic double imply.
DArrow :: CTL a -> CTL a -> CTL a
-- | It defines an atomic statement. E.g.: Atom "The plants look
-- great."
Atom :: a -> CTL a
Not :: CTL a -> CTL a
And :: CTL a -> CTL a -> CTL a
Or :: CTL a -> CTL a -> CTL a
-- | EX means that the CTL formula holds in at least one of
-- the inmediate successors states.
EX :: CTL a -> CTL a
-- | EF means that the CTL formula holds in at least one of
-- the future states.
EF :: CTL a -> CTL a
-- | EG means that the CTL formula holds always from one of
-- the future states.
EG :: CTL a -> CTL a
-- | AX means that the CTL formula holds in every one of the
-- inmediate successors states.
AX :: CTL a -> CTL a
-- | AF means that the CTL formula holds in at least one
-- state of every possible path.
AF :: CTL a -> CTL a
-- | AG means that the CTL formula holds in the current
-- states and all the successors in all paths. (It is true globally)
AG :: 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.
EU :: CTL a -> 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.
AU :: CTL a -> CTL a -> CTL a
-- | This is the function that implements the model checking algorithm for
-- CTL as defined by Queille, Sifakis, Clarke, Emerson and Sistla
-- 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 Int Bool
-- | This function returns the result of <math>.
modelsCTL :: Eq a => CTL a -> Automata -> AutomataInfo (CTL a) -> Bool
-- | 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]
instance GHC.Show.Show a => GHC.Show.Show (FSM.Logic.LTL a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (FSM.Logic.LTL a)
instance GHC.Show.Show a => GHC.Show.Show (FSM.Logic.CTL a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (FSM.Logic.CTL a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (FSM.Logic.LTL a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (FSM.Logic.CTL a)