{-+
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]