Safe Haskell	Safe-Inferred
Language	Haskell2010

SMCDEL.Explicit.S5

Synopsis

type World = Int
class HasWorlds a where
- worldsOf :: a -> [World]
type Partition = [[World]]
type Assignment = [(Prp, Bool)]
data KripkeModelS5 = KrMS5 [World] [(Agent, Partition)] [(World, Assignment)]
type PointedModelS5 = (KripkeModelS5, World)
type MultipointedModelS5 = (KripkeModelS5, [World])
newtype PropList = PropList [Prp]
withoutWorld :: KripkeModelS5 -> World -> KripkeModelS5
withoutProps :: KripkeModelS5 -> [Prp] -> KripkeModelS5
randomPartFor :: [World] -> Gen Partition
eval :: PointedModelS5 -> Form -> Bool
valid :: KripkeModelS5 -> Form -> Bool
announce :: PointedModelS5 -> [Agent] -> Form -> PointedModelS5
announceAction :: [Agent] -> [Agent] -> Form -> PointedActionModelS5
type Bisimulation = [(World, World)]
checkBisim :: Bisimulation -> KripkeModelS5 -> KripkeModelS5 -> Bool
checkBisimPointed :: Bisimulation -> PointedModelS5 -> PointedModelS5 -> Bool
generatedSubmodel :: PointedModelS5 -> PointedModelS5
bisimClasses :: KripkeModelS5 -> [[World]]
checkBisimClasses :: KripkeModelS5 -> Bool
bisiminimize :: PointedModelS5 -> PointedModelS5
type Action = Int
type PostCondition = [(Prp, Form)]
data ActionModelS5 = ActMS5 [(Action, (Form, PostCondition))] [(Agent, Partition)]
safepost :: PostCondition -> Prp -> Form
type PointedActionModelS5 = (ActionModelS5, Action)
type MultipointedActionModelS5 = (ActionModelS5, [Action])

Documentation

type World = Int Source #

class HasWorlds a where Source #

Methods

worldsOf :: a -> [World] Source #

Instances

Instances details

HasWorlds KripkeModel Source #
Instance details Defined in SMCDEL.Explicit.K Methods worldsOf :: KripkeModel -> [World] Source #
HasWorlds KripkeModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods worldsOf :: KripkeModelS5 -> [World] Source #
(HasWorlds a, Pointed a b) => HasWorlds (a, b) Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods worldsOf :: (a, b) -> [World] Source #

type Partition = [[World]] Source #

type Assignment = [(Prp, Bool)] Source #

data KripkeModelS5 Source #

Constructors

KrMS5 [World] [(Agent, Partition)] [(World, Assignment)]

Instances

Instances details

Arbitrary KripkeModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods arbitrary :: Gen KripkeModelS5 # shrink :: KripkeModelS5 -> [KripkeModelS5] #
Show KripkeModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods showsPrec :: Int -> KripkeModelS5 -> ShowS # show :: KripkeModelS5 -> String # showList :: [KripkeModelS5] -> ShowS #
Eq KripkeModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods (==) :: KripkeModelS5 -> KripkeModelS5 -> Bool # (/=) :: KripkeModelS5 -> KripkeModelS5 -> Bool #
Ord KripkeModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods compare :: KripkeModelS5 -> KripkeModelS5 -> Ordering # (<) :: KripkeModelS5 -> KripkeModelS5 -> Bool # (<=) :: KripkeModelS5 -> KripkeModelS5 -> Bool # (>) :: KripkeModelS5 -> KripkeModelS5 -> Bool # (>=) :: KripkeModelS5 -> KripkeModelS5 -> Bool # max :: KripkeModelS5 -> KripkeModelS5 -> KripkeModelS5 # min :: KripkeModelS5 -> KripkeModelS5 -> KripkeModelS5 #
HasWorlds KripkeModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods worldsOf :: KripkeModelS5 -> [World] Source #
KripkeLike KripkeModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods getNodes :: KripkeModelS5 -> [(String, String)] Source # getEdges :: KripkeModelS5 -> [(String, String, String)] Source # getActuals :: KripkeModelS5 -> [String] Source # directed :: KripkeModelS5 -> Bool Source # nodeAts :: KripkeModelS5 -> Bool -> Attributes Source # toGraph :: KripkeModelS5 -> DotGraph String Source # dispDot :: KripkeModelS5 -> IO () Source # textDot :: KripkeModelS5 -> Text Source # svg :: KripkeModelS5 -> String Source #
KripkeLike MultipointedModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods getNodes :: MultipointedModelS5 -> [(String, String)] Source # getEdges :: MultipointedModelS5 -> [(String, String, String)] Source # getActuals :: MultipointedModelS5 -> [String] Source # directed :: MultipointedModelS5 -> Bool Source # nodeAts :: MultipointedModelS5 -> Bool -> Attributes Source # toGraph :: MultipointedModelS5 -> DotGraph String Source # dispDot :: MultipointedModelS5 -> IO () Source # textDot :: MultipointedModelS5 -> Text Source # svg :: MultipointedModelS5 -> String Source #
KripkeLike PointedModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods getNodes :: PointedModelS5 -> [(String, String)] Source # getEdges :: PointedModelS5 -> [(String, String, String)] Source # getActuals :: PointedModelS5 -> [String] Source # directed :: PointedModelS5 -> Bool Source # nodeAts :: PointedModelS5 -> Bool -> Attributes Source # toGraph :: PointedModelS5 -> DotGraph String Source # dispDot :: PointedModelS5 -> IO () Source # textDot :: PointedModelS5 -> Text Source # svg :: PointedModelS5 -> String Source #
TexAble KripkeModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods tex :: KripkeModelS5 -> String Source # texTo :: KripkeModelS5 -> String -> IO () Source # texDocumentTo :: KripkeModelS5 -> String -> IO () Source # pdfTo :: KripkeModelS5 -> String -> IO () Source # disp :: KripkeModelS5 -> IO () Source # svgViaTex :: KripkeModelS5 -> String Source #
TexAble MultipointedModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods tex :: MultipointedModelS5 -> String Source # texTo :: MultipointedModelS5 -> String -> IO () Source # texDocumentTo :: MultipointedModelS5 -> String -> IO () Source # pdfTo :: MultipointedModelS5 -> String -> IO () Source # disp :: MultipointedModelS5 -> IO () Source # svgViaTex :: MultipointedModelS5 -> String Source #
TexAble PointedModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods tex :: PointedModelS5 -> String Source # texTo :: PointedModelS5 -> String -> IO () Source # texDocumentTo :: PointedModelS5 -> String -> IO () Source # pdfTo :: PointedModelS5 -> String -> IO () Source # disp :: PointedModelS5 -> IO () Source # svgViaTex :: PointedModelS5 -> String Source #
HasAgents KripkeModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods agentsOf :: KripkeModelS5 -> [Agent] Source #
HasVocab KripkeModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods vocabOf :: KripkeModelS5 -> [Prp] Source #
Optimizable PointedModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods optimize :: [Prp] -> PointedModelS5 -> PointedModelS5 Source #
Semantics KripkeModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods isTrue :: KripkeModelS5 -> Form -> Bool Source #
Semantics MultipointedModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods isTrue :: MultipointedModelS5 -> Form -> Bool Source #
Semantics PointedModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods isTrue :: PointedModelS5 -> Form -> Bool Source #
HasPerspective MultipointedModelS5 Source #	See ...
Instance details Defined in SMCDEL.Other.Planning Methods asSeenBy :: MultipointedModelS5 -> Agent -> MultipointedModelS5 Source # isLocalFor :: MultipointedModelS5 -> Agent -> Bool Source #
Pointed KripkeModelS5 World Source #
Instance details Defined in SMCDEL.Explicit.S5
Update KripkeModelS5 ActionModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods unsafeUpdate :: KripkeModelS5 -> ActionModelS5 -> KripkeModelS5 Source # checks :: [KripkeModelS5 -> ActionModelS5 -> Bool] Source # preCheck :: KripkeModelS5 -> ActionModelS5 -> Bool Source # update :: KripkeModelS5 -> ActionModelS5 -> KripkeModelS5 Source #
Update KripkeModelS5 Form Source #	Public announcements on Kripke models.
Instance details Defined in SMCDEL.Explicit.S5 Methods unsafeUpdate :: KripkeModelS5 -> Form -> KripkeModelS5 Source # checks :: [KripkeModelS5 -> Form -> Bool] Source # preCheck :: KripkeModelS5 -> Form -> Bool Source # update :: KripkeModelS5 -> Form -> KripkeModelS5 Source #
Update MultipointedModelS5 MultipointedActionModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods unsafeUpdate :: MultipointedModelS5 -> MultipointedActionModelS5 -> MultipointedModelS5 Source # checks :: [MultipointedModelS5 -> MultipointedActionModelS5 -> Bool] Source # preCheck :: MultipointedModelS5 -> MultipointedActionModelS5 -> Bool Source # update :: MultipointedModelS5 -> MultipointedActionModelS5 -> MultipointedModelS5 Source #
Update MultipointedModelS5 PointedActionModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods unsafeUpdate :: MultipointedModelS5 -> PointedActionModelS5 -> MultipointedModelS5 Source # checks :: [MultipointedModelS5 -> PointedActionModelS5 -> Bool] Source # preCheck :: MultipointedModelS5 -> PointedActionModelS5 -> Bool Source # update :: MultipointedModelS5 -> PointedActionModelS5 -> MultipointedModelS5 Source #
Update MultipointedModelS5 Form Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods unsafeUpdate :: MultipointedModelS5 -> Form -> MultipointedModelS5 Source # checks :: [MultipointedModelS5 -> Form -> Bool] Source # preCheck :: MultipointedModelS5 -> Form -> Bool Source # update :: MultipointedModelS5 -> Form -> MultipointedModelS5 Source #
Update PointedModelS5 MultipointedActionModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods unsafeUpdate :: PointedModelS5 -> MultipointedActionModelS5 -> PointedModelS5 Source # checks :: [PointedModelS5 -> MultipointedActionModelS5 -> Bool] Source # preCheck :: PointedModelS5 -> MultipointedActionModelS5 -> Bool Source # update :: PointedModelS5 -> MultipointedActionModelS5 -> PointedModelS5 Source #
Update PointedModelS5 PointedActionModelS5 Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods unsafeUpdate :: PointedModelS5 -> PointedActionModelS5 -> PointedModelS5 Source # checks :: [PointedModelS5 -> PointedActionModelS5 -> Bool] Source # preCheck :: PointedModelS5 -> PointedActionModelS5 -> Bool Source # update :: PointedModelS5 -> PointedActionModelS5 -> PointedModelS5 Source #
Update PointedModelS5 Form Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods unsafeUpdate :: PointedModelS5 -> Form -> PointedModelS5 Source # checks :: [PointedModelS5 -> Form -> Bool] Source # preCheck :: PointedModelS5 -> Form -> Bool Source # update :: PointedModelS5 -> Form -> PointedModelS5 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 KripkeModelS5 [World] Source #
Instance details Defined in SMCDEL.Explicit.S5

type PointedModelS5 = (KripkeModelS5, World) Source #

type MultipointedModelS5 = (KripkeModelS5, [World]) Source #

newtype PropList Source #

Constructors

PropList [Prp]

Instances

Instances details

Arbitrary PropList Source #
Instance details Defined in SMCDEL.Explicit.S5 Methods arbitrary :: Gen PropList # shrink :: PropList -> [PropList] #

withoutWorld :: KripkeModelS5 -> World -> KripkeModelS5 Source #

withoutProps :: KripkeModelS5 -> [Prp] -> KripkeModelS5 Source #

randomPartFor :: [World] -> Gen Partition Source #

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

valid :: KripkeModelS5 -> Form -> Bool Source #

announce :: PointedModelS5 -> [Agent] -> Form -> PointedModelS5 Source #

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

type Bisimulation = [(World, World)] Source #

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

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

generatedSubmodel :: PointedModelS5 -> PointedModelS5 Source #

bisimClasses :: KripkeModelS5 -> [[World]] Source #

checkBisimClasses :: KripkeModelS5 -> Bool Source #

bisiminimize :: PointedModelS5 -> PointedModelS5 Source #

type Action = Int Source #

type PostCondition = [(Prp, Form)] Source #

data ActionModelS5 Source #

Constructors

ActMS5 [(Action, (Form, PostCondition))] [(Agent, Partition)]

Instances

Instances details

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

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

A safe way to lookup all postconditions

type PointedActionModelS5 = (ActionModelS5, Action) Source #

type MultipointedActionModelS5 = (ActionModelS5, [Action]) Source #