ContentsIndex
MultiKnowledge.Theory
Contents
Syntax
Prog operations
Justifications
Various
Interfaces
Parse
Writing rules - MultiKnowledge specific functions
Rules
Description
This implements "A Refinement Theory that Supports Reasoning about Knowledge and Time for Synchronous Agents", April 6, 2005, by Kai Engelhardt, Ron van der Meyden, Yoram Moses.
Synopsis
module Core.Utils
module MultiKnowledge.KFormula
data KProg = KProg {
nAgents :: NumAgents
code :: (Code KSyn)
system :: KSystem
jt :: JT
}
type NumAgents = Maybe Int
data KSystem = KSystem
data KSyn
= Empty
| Action Action
| Seq
| Choice
| Omega
| Exists Int Variable
| Parallel
| Spec KFormula KFormula Tag
| Coercion KFormula Tag
| Assertion KFormula Tags
type Action = String
data Tag
= Fixed Int
| New Int
type Tags = [Tag]
checkProg :: KProg -> Maybe (NodeError KSyn)
kProgReplaceStep :: RegionApplyFun (KProg, Code KSyn -> Code KSyn)
kProgSelectStep :: RegionApplyFun KProg
type JT = Map Tag [Tag]
applyJT_ :: JT -> KProg -> KProg
freeIn :: Variable -> Code KSyn -> Bool
getChildNAgents :: KSyn -> NumAgents -> NumAgents
getDerivationJT :: Derivation KProg -> JT
mkKRule :: (forall m . MonadRule KProg m => m ()) -> String -> Doc -> Rule KProg
applyJT :: MonadRule KProg m => JT -> m ()
refines :: MonadRule KProg m => Code KSyn -> Code KSyn -> m (Derivation KProg)
choiceSpec_ :: MonadRule KProg m => m ()
parallelSpec_ :: MonadRule KProg m => m ()
loosenPost_ :: MonadRule KProg m => m ()
reduceND_ :: MonadRule KProg m => m ()
introCoercion_ :: MonadRule KProg m => m ()
elimAssertion_ :: MonadRule KProg m => m ()
introAssertion_ :: MonadRule KProg m => m ()
elimCoercion_ :: MonadRule KProg m => m ()
regressDiamond_ :: MonadRule KProg m => m ()
specCons_ :: MonadRule KProg m => m ()
introLocalProp_ :: MonadRule KProg m => m ()
seqSpec_ :: MonadRule KProg m => m ()
rules :: [Rule KProg]
Documentation
module Core.Utils
module MultiKnowledge.KFormula
Syntax
data KProg
Constructors
KProg
nAgents :: NumAgents
code :: (Code KSyn)
system :: KSystem
jt :: JTThe last justification transform applied to this program.
show/hide Instances
type NumAgents = Maybe Int
data KSystem
Constructors
KSystem
show/hide Instances
Show KSystem
Typeable KSystem
data KSyn
Syntactic elements used in program code FIXME: is Empty flawed?
Constructors
Empty
Action Action
Seq
Choice
Omega
Exists Int Variable
Parallel
Spec KFormula KFormula Tag
Coercion KFormula Tag
Assertion KFormula Tags
show/hide Instances
type Action = String
data Tag
Constraint tags. The program fed into a rule has all tags Fixed. When a rule creates a tag, it should create it as New - this will later be replaced by Fixed. The reason for this is to preserve uniqueness of tags after rule application.
Constructors
Fixed Int
New Int
show/hide Instances
Eq Tag
Ord Tag
Read Tag
Show Tag
type Tags = [Tag]
Prog operations
checkProg :: KProg -> Maybe (NodeError KSyn)

This functions defines what is a syntactically correct program.

1. Check that all tree nodes have proper number of children as required by their arities

2. Check that the program is parallel as defined in paper and that the number of agent programs is correct

kProgReplaceStep :: RegionApplyFun (KProg, Code KSyn -> Code KSyn)
kProgSelectStep :: RegionApplyFun KProg
Justifications
type JT = Map Tag [Tag]
Justification transformation, see paper. A correct justification shall not introduce any tags that are not present in some coercion or specification already. Any functions that work with JT may assume that it is correct.
applyJT_ :: JT -> KProg -> KProg

1. Apply the justification transformation to a program.

2. Change all New tags in specs and coercions to unique Fixed tags and update assertion justifications accordingly.

Various
freeIn :: Variable -> Code KSyn -> Bool
getChildNAgents :: KSyn -> NumAgents -> NumAgents
getDerivationJT :: Derivation KProg -> JT
Combines the JTs of all steps in the derivation into one.
Interfaces
Parse
Writing rules - MultiKnowledge specific functions
mkKRule
:: (forall m . MonadRule KProg m => m ())
-> Stringname
-> Docdescription
-> Rule KProg
applyJT :: MonadRule KProg m => JT -> m ()
refines :: MonadRule KProg m => Code KSyn -> Code KSyn -> m (Derivation KProg)
Rules
choiceSpec_ :: MonadRule KProg m => m ()
The rules trans and mon are not implemented explicitly but are implicit in the refinement tool.
parallelSpec_ :: MonadRule KProg m => m ()
loosenPost_ :: MonadRule KProg m => m ()
reduceND_ :: MonadRule KProg m => m ()
introCoercion_ :: MonadRule KProg m => m ()
elimAssertion_ :: MonadRule KProg m => m ()
introAssertion_ :: MonadRule KProg m => m ()
elimCoercion_ :: MonadRule KProg m => m ()
regressDiamond_ :: MonadRule KProg m => m ()
specCons_ :: MonadRule KProg m => m ()
introLocalProp_ :: MonadRule KProg m => m ()
seqSpec_ :: MonadRule KProg m => m ()
rules :: [Rule KProg]
Produced by Haddock version 0.8