Model.hs

Models

module Model(module Model,enumAll) where
import Extra(enumAll,Trans(..))

A state transition model of a system consists of four parts:

• S: the set of states
• R: the state transition relation
• A: the set of atomic formulas
• L: a function that tells which atomic formulas are true in which states

Here, S and A are represented as types, R and L as functions.

data Model a s                   -- A, S
    = Model {
        next :: s -> [s],        -- R
        atom :: a -> s -> Bool   -- L
      }

A function to compute the previous states

--prev :: ... => Model a s -> s -> [s]

prev m s2 = [s1|s1<-enumAll,s2 `elem` next m s1] -- quick hack

A function to list the state transitions of a model

-- transitions :: ... => Model a s -> [Trans s [s]]

transitions m = [s:->next m s|s<-enumAll]