Safe Haskell	Safe-Inferred
Language	Haskell2010

SMCDEL.Explicit.K

Synopsis

newtype KripkeModel = KrM (Map World (Map Prp Bool, Map Agent [World]))
type PointedModel = (KripkeModel, World)
type MultipointedModel = (KripkeModel, [World])
distinctVal :: KripkeModel -> Bool
relOfIn :: Agent -> KripkeModel -> Map World [World]
truthsInAt :: KripkeModel -> World -> [Prp]
withoutWorld :: KripkeModel -> World -> KripkeModel
eval :: PointedModel -> Form -> Bool
groupRel :: KripkeModel -> [Agent] -> World -> [World]
distRel :: KripkeModel -> [Agent] -> World -> [World]
announceAction :: [Agent] -> [Agent] -> Form -> PointedActionModel
checkBisim :: Bisimulation -> KripkeModel -> KripkeModel -> Bool
checkBisimPointed :: Bisimulation -> PointedModel -> PointedModel -> Bool
type Status = Maybe Form
type StatusMap = Map (World, World) Status
diff :: KripkeModel -> KripkeModel -> StatusMap
diffPointed :: PointedModel -> PointedModel -> Either Bisimulation Form
generatedSubmodel :: PointedModel -> PointedModel
type PostCondition = Map Prp Form
data Act = Act {
- pre :: Form
- post :: PostCondition
- rel :: Map Agent [Action]
}
safepost :: Act -> Prp -> Form
newtype ActionModel = ActM (Map Action Act)
type PointedActionModel = (ActionModel, Action)
type MultipointedActionModel = (ActionModel, [Action])

Documentation

newtype KripkeModel Source #

Constructors

KrM (Map World (Map Prp Bool, Map Agent [World]))

Instances

Instances details

Arbitrary KripkeModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods arbitrary :: Gen KripkeModel # shrink :: KripkeModel -> [KripkeModel] #
Show KripkeModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods showsPrec :: Int -> KripkeModel -> ShowS # show :: KripkeModel -> String # showList :: [KripkeModel] -> ShowS #
Eq KripkeModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods (==) :: KripkeModel -> KripkeModel -> Bool # (/=) :: KripkeModel -> KripkeModel -> Bool #
Ord KripkeModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods compare :: KripkeModel -> KripkeModel -> Ordering # (<) :: KripkeModel -> KripkeModel -> Bool # (<=) :: KripkeModel -> KripkeModel -> Bool # (>) :: KripkeModel -> KripkeModel -> Bool # (>=) :: KripkeModel -> KripkeModel -> Bool # max :: KripkeModel -> KripkeModel -> KripkeModel # min :: KripkeModel -> KripkeModel -> KripkeModel #
HasWorlds KripkeModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods worldsOf :: KripkeModel -> [World] Source #
KripkeLike KripkeModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods getNodes :: KripkeModel -> [(String, String)] Source # getEdges :: KripkeModel -> [(String, String, String)] Source # getActuals :: KripkeModel -> [String] Source # directed :: KripkeModel -> Bool Source # nodeAts :: KripkeModel -> Bool -> Attributes Source # toGraph :: KripkeModel -> DotGraph String Source # dispDot :: KripkeModel -> IO () Source # textDot :: KripkeModel -> Text Source # svg :: KripkeModel -> String Source #
KripkeLike MultipointedModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods getNodes :: MultipointedModel -> [(String, String)] Source # getEdges :: MultipointedModel -> [(String, String, String)] Source # getActuals :: MultipointedModel -> [String] Source # directed :: MultipointedModel -> Bool Source # nodeAts :: MultipointedModel -> Bool -> Attributes Source # toGraph :: MultipointedModel -> DotGraph String Source # dispDot :: MultipointedModel -> IO () Source # textDot :: MultipointedModel -> Text Source # svg :: MultipointedModel -> String Source #
KripkeLike PointedModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods getNodes :: PointedModel -> [(String, String)] Source # getEdges :: PointedModel -> [(String, String, String)] Source # getActuals :: PointedModel -> [String] Source # directed :: PointedModel -> Bool Source # nodeAts :: PointedModel -> Bool -> Attributes Source # toGraph :: PointedModel -> DotGraph String Source # dispDot :: PointedModel -> IO () Source # textDot :: PointedModel -> Text Source # svg :: PointedModel -> String Source #
TexAble KripkeModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods tex :: KripkeModel -> String Source # texTo :: KripkeModel -> String -> IO () Source # texDocumentTo :: KripkeModel -> String -> IO () Source # pdfTo :: KripkeModel -> String -> IO () Source # disp :: KripkeModel -> IO () Source # svgViaTex :: KripkeModel -> String Source #
TexAble MultipointedModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods tex :: MultipointedModel -> String Source # texTo :: MultipointedModel -> String -> IO () Source # texDocumentTo :: MultipointedModel -> String -> IO () Source # pdfTo :: MultipointedModel -> String -> IO () Source # disp :: MultipointedModel -> IO () Source # svgViaTex :: MultipointedModel -> String Source #
TexAble PointedModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods tex :: PointedModel -> String Source # texTo :: PointedModel -> String -> IO () Source # texDocumentTo :: PointedModel -> String -> IO () Source # pdfTo :: PointedModel -> String -> IO () Source # disp :: PointedModel -> IO () Source # svgViaTex :: PointedModel -> String Source #
HasAgents KripkeModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods agentsOf :: KripkeModel -> [Agent] Source #
HasVocab KripkeModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods vocabOf :: KripkeModel -> [Prp] Source #
Semantics KripkeModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods isTrue :: KripkeModel -> Form -> Bool Source #
Semantics MultipointedModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods isTrue :: MultipointedModel -> Form -> Bool Source #
Semantics PointedModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods isTrue :: PointedModel -> Form -> Bool Source #
HasPerspective MultipointedModel Source #	Here we also implement perspective shifts in K. The authors of [EBMN 2017] only consider S5. Given a multipointed Kripke model $(M,s)$, let the local state of $i$ be: \[ s^i := \{ w \in W \mid \exists v \in s : v R_i w \} \] Intuitively, these are all worlds the agent considers possible if the current state is $s$.
Instance details Defined in SMCDEL.Other.Planning Methods asSeenBy :: MultipointedModel -> Agent -> MultipointedModel Source # isLocalFor :: MultipointedModel -> Agent -> Bool Source #
Pointed KripkeModel World Source #
Instance details Defined in SMCDEL.Explicit.K
Update KripkeModel ActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods unsafeUpdate :: KripkeModel -> ActionModel -> KripkeModel Source # checks :: [KripkeModel -> ActionModel -> Bool] Source # preCheck :: KripkeModel -> ActionModel -> Bool Source # update :: KripkeModel -> ActionModel -> KripkeModel Source #
Update KripkeModel Form Source #
Instance details Defined in SMCDEL.Explicit.K Methods unsafeUpdate :: KripkeModel -> Form -> KripkeModel Source # checks :: [KripkeModel -> Form -> Bool] Source # preCheck :: KripkeModel -> Form -> Bool Source # update :: KripkeModel -> Form -> KripkeModel Source #
Update MultipointedModel MultipointedActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods unsafeUpdate :: MultipointedModel -> MultipointedActionModel -> MultipointedModel Source # checks :: [MultipointedModel -> MultipointedActionModel -> Bool] Source # preCheck :: MultipointedModel -> MultipointedActionModel -> Bool Source # update :: MultipointedModel -> MultipointedActionModel -> MultipointedModel Source #
Update MultipointedModel PointedActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods unsafeUpdate :: MultipointedModel -> PointedActionModel -> MultipointedModel Source # checks :: [MultipointedModel -> PointedActionModel -> Bool] Source # preCheck :: MultipointedModel -> PointedActionModel -> Bool Source # update :: MultipointedModel -> PointedActionModel -> MultipointedModel Source #
Update MultipointedModel Form Source #
Instance details Defined in SMCDEL.Explicit.K Methods unsafeUpdate :: MultipointedModel -> Form -> MultipointedModel Source # checks :: [MultipointedModel -> Form -> Bool] Source # preCheck :: MultipointedModel -> Form -> Bool Source # update :: MultipointedModel -> Form -> MultipointedModel Source #
Update PointedModel MultipointedActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods unsafeUpdate :: PointedModel -> MultipointedActionModel -> PointedModel Source # checks :: [PointedModel -> MultipointedActionModel -> Bool] Source # preCheck :: PointedModel -> MultipointedActionModel -> Bool Source # update :: PointedModel -> MultipointedActionModel -> PointedModel Source #
Update PointedModel PointedActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods unsafeUpdate :: PointedModel -> PointedActionModel -> PointedModel Source # checks :: [PointedModel -> PointedActionModel -> Bool] Source # preCheck :: PointedModel -> PointedActionModel -> Bool Source # update :: PointedModel -> PointedActionModel -> PointedModel Source #
Update PointedModel Form Source #
Instance details Defined in SMCDEL.Explicit.K Methods unsafeUpdate :: PointedModel -> Form -> PointedModel Source # checks :: [PointedModel -> Form -> Bool] Source # preCheck :: PointedModel -> Form -> Bool Source # update :: PointedModel -> Form -> PointedModel Source #
Convertable PointedModelS5 PointedModel Source #	Every S5 Kripke model is also a general Kripke model. This replaces each partition $\sim_i$ with a relation $R_i$.
Instance details Defined in SMCDEL.Translations.Convert Methods convert :: PointedModelS5 -> PointedModel Source #
Pointed KripkeModel [World] Source #
Instance details Defined in SMCDEL.Explicit.K

type PointedModel = (KripkeModel, World) Source #

type MultipointedModel = (KripkeModel, [World]) Source #

distinctVal :: KripkeModel -> Bool Source #

relOfIn :: Agent -> KripkeModel -> Map World [World] Source #

truthsInAt :: KripkeModel -> World -> [Prp] Source #

withoutWorld :: KripkeModel -> World -> KripkeModel Source #

eval :: PointedModel -> Form -> Bool Source #

groupRel :: KripkeModel -> [Agent] -> World -> [World] Source #

Transitive closure of the union of the relations of a group. Note that this is not necessarily reflexive.

distRel :: KripkeModel -> [Agent] -> World -> [World] Source #

announceAction :: [Agent] -> [Agent] -> Form -> PointedActionModel Source #

checkBisim :: Bisimulation -> KripkeModel -> KripkeModel -> Bool Source #

checkBisimPointed :: Bisimulation -> PointedModel -> PointedModel -> Bool Source #

type Status = Maybe Form Source #

type StatusMap = Map (World, World) Status Source #

diff :: KripkeModel -> KripkeModel -> StatusMap Source #

diffPointed :: PointedModel -> PointedModel -> Either Bisimulation Form Source #

generatedSubmodel :: PointedModel -> PointedModel Source #

type PostCondition = Map Prp Form Source #

data Act Source #

Constructors

Act
Fields pre :: Form post :: PostCondition rel :: Map Agent [Action]

Instances

Instances details

Show Act Source #
Instance details Defined in SMCDEL.Explicit.K Methods showsPrec :: Int -> Act -> ShowS # show :: Act -> String # showList :: [Act] -> ShowS #
Eq Act Source #
Instance details Defined in SMCDEL.Explicit.K Methods (==) :: Act -> Act -> Bool # (/=) :: Act -> Act -> Bool #
Ord Act Source #
Instance details Defined in SMCDEL.Explicit.K Methods compare :: Act -> Act -> Ordering # (<) :: Act -> Act -> Bool # (<=) :: Act -> Act -> Bool # (>) :: Act -> Act -> Bool # (>=) :: Act -> Act -> Bool # max :: Act -> Act -> Act # min :: Act -> Act -> Act #

safepost :: Act -> Prp -> Form Source #

Extend post to all propositions

newtype ActionModel Source #

Constructors

ActM (Map Action Act)

Instances

Instances details

Arbitrary ActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods arbitrary :: Gen ActionModel # shrink :: ActionModel -> [ActionModel] #
Show ActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods showsPrec :: Int -> ActionModel -> ShowS # show :: ActionModel -> String # showList :: [ActionModel] -> ShowS #
Eq ActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods (==) :: ActionModel -> ActionModel -> Bool # (/=) :: ActionModel -> ActionModel -> Bool #
Ord ActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods compare :: ActionModel -> ActionModel -> Ordering # (<) :: ActionModel -> ActionModel -> Bool # (<=) :: ActionModel -> ActionModel -> Bool # (>) :: ActionModel -> ActionModel -> Bool # (>=) :: ActionModel -> ActionModel -> Bool # max :: ActionModel -> ActionModel -> ActionModel # min :: ActionModel -> ActionModel -> ActionModel #
KripkeLike ActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods getNodes :: ActionModel -> [(String, String)] Source # getEdges :: ActionModel -> [(String, String, String)] Source # getActuals :: ActionModel -> [String] Source # directed :: ActionModel -> Bool Source # nodeAts :: ActionModel -> Bool -> Attributes Source # toGraph :: ActionModel -> DotGraph String Source # dispDot :: ActionModel -> IO () Source # textDot :: ActionModel -> Text Source # svg :: ActionModel -> String Source #
KripkeLike MultipointedActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods getNodes :: MultipointedActionModel -> [(String, String)] Source # getEdges :: MultipointedActionModel -> [(String, String, String)] Source # getActuals :: MultipointedActionModel -> [String] Source # directed :: MultipointedActionModel -> Bool Source # nodeAts :: MultipointedActionModel -> Bool -> Attributes Source # toGraph :: MultipointedActionModel -> DotGraph String Source # dispDot :: MultipointedActionModel -> IO () Source # textDot :: MultipointedActionModel -> Text Source # svg :: MultipointedActionModel -> String Source #
KripkeLike PointedActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods getNodes :: PointedActionModel -> [(String, String)] Source # getEdges :: PointedActionModel -> [(String, String, String)] Source # getActuals :: PointedActionModel -> [String] Source # directed :: PointedActionModel -> Bool Source # nodeAts :: PointedActionModel -> Bool -> Attributes Source # toGraph :: PointedActionModel -> DotGraph String Source # dispDot :: PointedActionModel -> IO () Source # textDot :: PointedActionModel -> Text Source # svg :: PointedActionModel -> String Source #
TexAble ActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods tex :: ActionModel -> String Source # texTo :: ActionModel -> String -> IO () Source # texDocumentTo :: ActionModel -> String -> IO () Source # pdfTo :: ActionModel -> String -> IO () Source # disp :: ActionModel -> IO () Source # svgViaTex :: ActionModel -> String Source #
TexAble MultipointedActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods tex :: MultipointedActionModel -> String Source # texTo :: MultipointedActionModel -> String -> IO () Source # texDocumentTo :: MultipointedActionModel -> String -> IO () Source # pdfTo :: MultipointedActionModel -> String -> IO () Source # disp :: MultipointedActionModel -> IO () Source # svgViaTex :: MultipointedActionModel -> String Source #
TexAble PointedActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods tex :: PointedActionModel -> String Source # texTo :: PointedActionModel -> String -> IO () Source # texDocumentTo :: PointedActionModel -> String -> IO () Source # pdfTo :: PointedActionModel -> String -> IO () Source # disp :: PointedActionModel -> IO () Source # svgViaTex :: PointedActionModel -> String Source #
HasAgents ActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods agentsOf :: ActionModel -> [Agent] Source #
HasPrecondition ActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods preOf :: ActionModel -> Form Source #
HasPrecondition MultipointedActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods preOf :: MultipointedActionModel -> Form Source #
HasPrecondition PointedActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods preOf :: PointedActionModel -> Form Source #
Pointed ActionModel Action Source #
Instance details Defined in SMCDEL.Explicit.K
Update KripkeModel ActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods unsafeUpdate :: KripkeModel -> ActionModel -> KripkeModel Source # checks :: [KripkeModel -> ActionModel -> Bool] Source # preCheck :: KripkeModel -> ActionModel -> Bool Source # update :: KripkeModel -> ActionModel -> KripkeModel Source #
Update MultipointedModel MultipointedActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods unsafeUpdate :: MultipointedModel -> MultipointedActionModel -> MultipointedModel Source # checks :: [MultipointedModel -> MultipointedActionModel -> Bool] Source # preCheck :: MultipointedModel -> MultipointedActionModel -> Bool Source # update :: MultipointedModel -> MultipointedActionModel -> MultipointedModel Source #
Update MultipointedModel PointedActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods unsafeUpdate :: MultipointedModel -> PointedActionModel -> MultipointedModel Source # checks :: [MultipointedModel -> PointedActionModel -> Bool] Source # preCheck :: MultipointedModel -> PointedActionModel -> Bool Source # update :: MultipointedModel -> PointedActionModel -> MultipointedModel Source #
Update PointedModel MultipointedActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods unsafeUpdate :: PointedModel -> MultipointedActionModel -> PointedModel Source # checks :: [PointedModel -> MultipointedActionModel -> Bool] Source # preCheck :: PointedModel -> MultipointedActionModel -> Bool Source # update :: PointedModel -> MultipointedActionModel -> PointedModel Source #
Update PointedModel PointedActionModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods unsafeUpdate :: PointedModel -> PointedActionModel -> PointedModel Source # checks :: [PointedModel -> PointedActionModel -> Bool] Source # preCheck :: PointedModel -> PointedActionModel -> Bool Source # update :: PointedModel -> PointedActionModel -> PointedModel Source #
Pointed ActionModel [Action] Source #
Instance details Defined in SMCDEL.Explicit.K

type PointedActionModel = (ActionModel, Action) Source #

type MultipointedActionModel = (ActionModel, [Action]) Source #