moduleMCwhereimportIximportData.Set-- a library data type for setsimportCTLimportModel

The model checking function `mc` takes a model and a CTL formula and returns
the set of states in which the formula is true.

```
--mc :: ... => Model a s -> CTL a -> Set s
```

mcmp=casepofAtoma->fromList[s|s<-enumAll,atommas]Notp->complement(mcmp)Orpq->mcmp`union`mcmqEXp->img_prevm$mcmpEFp->lfp(\s->s0`union`img_prevms)wheres0=mcmpEGp->gfp(\s->s0`intersection`img_prevms)wheres0=mcmpEUpq->lfp(\s->qs`union` (ps`intersection`img_prevms))whereps=mcmpqs=mcmq

Set complement

```
--complement :: ... => Set s -> Set s -> Set s
```

complements=differenceuniversesuniverse::(Boundeds,Ixs)=>Setsuniverse=fromListenumAll

Compute the backward image of a set of states, e.g. the preceeding states
according to the state transition relation.
(This function is called Image^{-1}(S,R) in the slides.)

```
-- img_prev :: ... => Model a s -> Set s -> Set s
```

img_prevm=fromList.concatMap(prevm).toList

Fixed point iteration: `lfp` (least fixed point) starts from the empty set.
`gfp` (greatest fixed point) starts from the universe. The function `f` should
be monotonic.

```
-- lfp, gfl :: (Set s->Set s)->Set s
```

lfpf=fixfemptygfpf=fixfuniversefix::(Eqx)=>(x->x)->x->xfixfx=ifx'==xthenxelsefixfx'wherex'=fx