#]W<      !"#$%&'()*+,-./0123456789:;NoneAzFSMThis 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.6Please pay attention to how the object is built. E.g., createAutomata s i s0 m awhere:*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: )2a 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]FSM 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. FSMThis 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.FSM@This function returns the current initial state of the automata.FSMTThis function returns the string of inputs (alphabet) that the automata accepts. FSMvThis 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  3https://en.wikipedia.org/wiki/Lexicographical_orderlexicographical order.OThe rows of the matrix represent the states of the automata in ascending order. 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: 4https://en.wikipedia.org/wiki/State-transition_table!Wikipedia: State-transition tableeContinuing with the previous example, the following matrix correspongs to the automata in the figure. smat = 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 ^ | statesJAnd the matrix above represents the transitions in the following automata: https://i.imgur.com/ymWLlsb.pngTom automata figureFSM[This function returns the inputs that a state accepts for transitioning into another state.FSMKThis function returns the states you can possibly reach from a given state. FSMGThis function returns the states that can possibly reach a given state. FSMThis 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. FSMNThis function returns the states of the given automata that cannot be reached. FSM"This function test if a string is validV, i.e., if when the automata receives the string, ends in one of the accepting states. FSMFunction 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. FSMThis 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.FSM(This function changes the initial state.FSM&This function adds one accepting state  Safe^FSMThis 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" 259If you created your own data type, you can do as follows: ,my_info = createStateInfo 4 "tag" (Type2 25)FSMXThis 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)FSMbThis function returns the states of the given AutomataInfo that currently contain some informationFSMRThis function returns the tags that a given state contains inside the AutomataInfoFSMGThis function returns the information contained in the given state. If NothingE is given, then it returns all the information in the state while if Just tagJ is given, it will return only the information inside the given tag. E.g: FgetInfoInState my_info 4 Nothing getInfoInState my_info 4 (Just "foo")FSMThis 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: 0alterStateInfo 3 (Just "foo") (Type2 45) my_infoFSM~This function takes the left-biased union of t1 and t2. It prefers t1 when duplicate keys are encountered. Works similarly to  Thttp://hackage.haskell.org/package/containers-0.6.2.1/docs/Data-Map-Strict.html#g:12Data.Map.union.  NoneT<FSM*It defines an atomic statement. E.g.: ' "The plants look great."=FSM+ means that the "B formula holds in at least one of the inmediate successors states.>FSM, means that the "4 formula holds in at least one of the future states.?FSM- means that the "4 formula holds always from one of the future states.@FSM1J means that exists a path from the current state that satisfies the first " formula until; it reaches a state in that path that satisfies the second " formula."FSMWThis is the definition of the CTL language. More info about this language can be found  4https://en.wikipedia.org/wiki/Computation_tree_logichereH. You can find the details of the constructors in the definition of the " data.KHere you can find a visual explanation of the constructors defined below. https://i.imgur.com/e4tPiOY.jpg CTL examples Chttps://www.researchgate.net/figure/CTL-tree-logic-1_fig6_257343964SourceC: A SAFE COTS-BASED DESIGN FLOW OF EMBEDDED SYSTEMS by Salam Hajjar$FSM Basic bools.%FSM Basic imply.&FSMBasic double imply.'FSM*It defines an atomic statement. E.g.: ' "The plants look great."+FSM+ means that the "B formula holds in at least one of the inmediate successors states.,FSM, means that the "4 formula holds in at least one of the future states.-FSM- means that the "4 formula holds always from one of the future states..FSM. means that the "? formula holds in every one of the inmediate successors states./FSM/ means that the "< formula holds in at least one state of every possible path.0FSM0 means that the "_ formula holds in the current states and all the successors in all paths. (It is true globally)1FSM1J means that exists a path from the current state that satisfies the first " formula until; it reaches a state in that path that satisfies the second " formula.2FSM2B means that every path from the current state satisfies the first " formula until. it reaches a state that satisfies the second " formula.3FSMThis 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.5399here and that was later improved. %This function takes as an argument a " formula, an 0 and information about the states as defined in  FSM.Automata and  FSM.States% respectively and checks whether the  implies the " 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  ) (checkCTL "  ) 4FSM$This function returns the result of automata \models formula .5FSM]This function loops over multiple formulas and tells you if the automata models each formula."(#$%&')*+,-./012345"(#$%&')*+,-./012345Safe2ABCDEFGHI      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNFSM-1.0.0-TeH8aMBfd1GrNrr3EkCum FSM.Automata FSM.States FSM.Logic Paths_FSMAutomatacreateAutomata getStatesgetAcceptingStatesgetInitialState getInputsgetAssociationsgetTransitionsgetOutgoingStatesgetIncomingStates getDeadlocks getIsolated validInputaddState deleteStatechangeInitialStateaddAcceptingState$fShowAutomata AutomataInfo StateInfoTagStatecreateStateInfofromlsStateInfo getStateInfogetStatesWithInfogetTagsInStategetInfoInStatealterStateInfounionStateInfo$fShowStateInfo$fShowAutomataInfo $fEqStateInfo$fEqAutomataInfoCTLCTrueCFalseRArrowDArrowAtomNotAndOrEXEFEGAXAFAGEUAUcheckCTL modelsCTL checkFormulas$fEqCTL$fEqLTL$fOrdCTL $fShowCTL$fOrdLTL $fShowLTLLTL_AtomLTL_XLTL_FLTL_GLTL_Uversion getBinDir getLibDir getDynLibDir getDataDir getLibexecDir getSysconfDirgetDataFileName