moduleModel(moduleModel,enumAll)whereimportExtra(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.

dataModelas-- A, S=Model{next::s->[s], -- Ratom::a->s->Bool-- L }

A function to compute the previous states

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

prevms2=[s1|s1<-enumAll,s2`elem`nextms1] -- quick hack

A function to list the state transitions of a model

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

transitionsm=[s:->nextms|s<-enumAll]