|
|
|
|
|
| Description |
| This module defines Kripke models,
and the evaluation of terms inside these models.
|
|
| Synopsis |
|
|
|
| Documentation |
|
| data Model world |
| A Kripke model, the worlds are of the type world
| | Constructors | | Model | | | modValuation :: (Map world (Map VarName Bool)) | A valuation, in what world are what variables true/false?
| | modRelations :: (Map Agents (Relation world)) | Accessability relations for each agent
| | modRoot :: world | The root world of the model, terms are evalutated here
|
|
|  Instances | |
|
|
| modWorlds :: Model w -> [w] |
| All worlds in a Kripke model
|
|
| modIsWorld :: Ord w => w -> Model w -> Bool |
| Does the given world actually exist?
|
|
| Evaluation
|
|
| class Models a where |
Evaluating terms in a model.
- m |= t evaluates t in the root world of the model.
- (m,w) |= t evaluates t in the world w of the model.
| | | Methods | | (|=) :: a -> Formula -> Bool | | m |= term should be read as "m models term".
Does the term evaluate to True in the model?
| | | (|/=) :: a -> Formula -> Bool | | Does not model
|
| | | Instances | |
|
|
| annotate :: Model Int -> Program -> Program |
| Annotate each subformula of a Program with a Note that specifies in what worlds that formula is true.
|
|
| Transformations
|
|
| toIntKeys :: Ord w => Model w -> Model Int |
| Use integer keys for a model.
This allows for faster computation, and for correct graphviz conversion.
|
|
| simplifyModel :: Ord w => (Model w -> Bool) -> Model w -> Model w |
| Simplfy a model by merging worlds.
Ensures that the model still satisfies a predicate
|
|
| axiomaticClosure :: Ord w => Set Agents -> Axioms -> Model w -> Model w |
| Take the reflexive, transitive, symmetric closure of a counter model,
but only as needed by the axioms.
|
|
| transSymClosure :: Ord w => Model w -> Model w |
| Take the reflexive, transitive, symmetric closure of a counter model
|
|
| addReflexive :: Ord w => Set Agents -> Model w -> Model w |
| Add reflexive arrows for the given set of agents,
only add arrows to worlds without outgoing ones.
|
|
| Produced by Haddock version 0.8 |
