| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
SMCDEL.Examples
Description
This module shows how to use the SMCDEL model checker and the translations with some toy examples.
Synopsis
- modelA :: PointedModelS5
- modelB :: PointedModelS5
- knsA :: KnowScene
- knsB :: KnowScene
- redundantModel :: PointedModelS5
- myKNS :: KnowScene
- minimizedModel :: PointedModelS5
- minimizedKNS :: KnowScene
- myPropu :: Propulation
- pubAnnounceAction :: [Agent] -> Form -> PointedActionModelS5
- examplePaAction :: PointedActionModelS5
- groupAnnounceAction :: [Agent] -> [Agent] -> Form -> PointedActionModelS5
- exampleGroupAnnounceAction :: PointedActionModelS5
- eGrAnLaw :: Form
- exampleGrAnnEvent :: Event
- actionOne :: PointedActionModelS5
- actionTwo :: PointedActionModelS5
Knowledge and Meta-Knowledge
modelA :: PointedModelS5 Source #
A Kripke model with two states, where Bob knows that \(p\) is true and Alice does not. Still, Alice knows that Bob knows whether \(p\). This is because in all worlds that Alice confuses with the actual world Bob either knows that \(p\) or he knows that not \(p\).
modelB :: PointedModelS5 Source #
A model with three states. Bob knows that \(p\) is true and Alice does not. Additionally here Alice does not even know whether Bob knows whether \(p\).
The only difference is in the state law of the knowledge structures.
Remember that this component determines which assignments are states of this knowledge structure.
In our implementation this is not a formula but a BDD, hence we show its graph here.
The BDD in knsA demands that the propositions \(p\) and \(p_2\) have the same value.
Hence knsA has just two states while knsB has three:
>>>let (structA,foo) = knsA in statesOf structA[[P 0,P 2],[]]
>>>let (structB,foo) = knsB in statesOf structB[[P 0],[P 0,P 2],[]]
Minimization via Translation
redundantModel :: PointedModelS5 Source #
A Kripke model with three states 0,1,2 where 0 and 1 are bisimilar --- it is redundant.
The knowledge structure equivalent to redundantModel.
myPropu :: Propulation Source #
A propulation between myKNS and minimizedKNS.
Different Announcements
pubAnnounceAction :: [Agent] -> Form -> PointedActionModelS5 Source #
Public announcement as an action model.
groupAnnounceAction :: [Agent] -> [Agent] -> Form -> PointedActionModelS5 Source #
Group announcement as an action model.
Equivalent Action Models
actionOne :: PointedActionModelS5 Source #
An action model.
actionTwo :: PointedActionModelS5 Source #
Another action model which has bisimilar (in fact identical!) effects as actionOne on any Kripke model.