| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
SMCDEL.Translations.S5
Description
Converting between S5 Kripke Models and Knowledge Structures
In this module we define and implement translation methods to connect the semantics from the two previous sections. This essentially allows us to switch back and forth between explicit and symbolic model checking methods.
Synopsis
- type StateMap = World -> State
- equivalentWith :: PointedModelS5 -> KnowScene -> StateMap -> Bool
- findStateMap :: PointedModelS5 -> KnowScene -> Maybe StateMap
- knsToKripke :: KnowScene -> PointedModelS5
- knsToKripkeWithG :: KnowStruct -> (KripkeModelS5, StateMap)
- knsToKripkeMulti :: MultipointedKnowScene -> MultipointedModelS5
- kripkeToKns :: PointedModelS5 -> KnowScene
- kripkeToKnsWithG :: KripkeModelS5 -> (KnowStruct, StateMap)
- booloutof :: [Prp] -> [Prp] -> Bdd
- kripkeToKnsMulti :: MultipointedModelS5 -> MultipointedKnowScene
- uniqueVals :: KripkeModelS5 -> Bool
- obsnobs :: KripkeModelS5 -> Agent -> ([Prp], [Prp])
- descableRels :: KripkeModelS5 -> Bool
- smartKripkeToKns :: PointedModelS5 -> Maybe KnowScene
- smartKripkeToKnsWithoutChecks :: PointedModelS5 -> KnowScene
- transformerToActionModelWithG :: KnowTransformer -> (ActionModelS5, StateMap)
- eventToAction :: Event -> PointedActionModelS5
- eventToActionMulti :: MultipointedEvent -> MultipointedActionModelS5
- actionToTransformerWithMap :: ActionModelS5 -> (KnowTransformer, StateMap)
- actionToEvent :: PointedActionModelS5 -> Event
- actionToEventMulti :: MultipointedActionModelS5 -> MultipointedEvent
Tools for Equivalence
equivalentWith :: PointedModelS5 -> KnowScene -> StateMap -> Bool Source #
findStateMap :: PointedModelS5 -> KnowScene -> Maybe StateMap Source #
From Knowledge Structures to S5 Kripke Models
knsToKripkeWithG :: KnowStruct -> (KripkeModelS5, StateMap) Source #
From S5 Kripke Models to Knowledge Structures
kripkeToKnsWithG :: KripkeModelS5 -> (KnowStruct, StateMap) Source #
booloutof :: [Prp] -> [Prp] -> Bdd Source #
BDD to say that exactly this subset of a given vocabulary is true.
kripkeToKnsMulti :: MultipointedModelS5 -> MultipointedKnowScene Source #
Convert a multipointed S5 Kripke model to a knoweldge structure.
See also smartKripkeToKns.
uniqueVals :: KripkeModelS5 -> Bool Source #
obsnobs :: KripkeModelS5 -> Agent -> ([Prp], [Prp]) Source #
Get lists of variables which agent i does (not) observe in model m. This does *not* preserve all information, i.e. does not characterize every possible S5 relation!
descableRels :: KripkeModelS5 -> Bool Source #
Test if all relations can be described using observariables.
smartKripkeToKns :: PointedModelS5 -> Maybe KnowScene Source #
Try to find an equivalent knowledge structure without
additional propositions. Will succeed iff valuations are
unique and relations can be described using observariables.
This is an alternative to kripkeToKnsMulti.
smartKripkeToKnsWithoutChecks :: PointedModelS5 -> KnowScene Source #
Unsafe version of smartKripkeToKns.