Datatype

A sequent with a conjunction of a set of facts as the premise and a single formula as the conclusion denoting a statement about a reachable state of a protocol.

Constructors

Sequent
Fields sePrem :: Facts seConcl :: Formula

Instances

Eq Sequent
Data Sequent
Ord Sequent
Show Sequent
Typeable Sequent

seProto :: Sequent -> Protocol Source

The protocol of a sequent.

Logically safe construction

wellTypedCases :: MonadPlus m => Sequent -> m [(String, Sequent)]Source

The named list of sequents which need to be proven in order to prove that the given protocol is well typed or weakly-atomic

PRE: The conclusion of the sequent must be typing atom.

Uses fail for error reporting.

saturate :: MonadPlus m => Sequent -> m Sequent Source

Try to saturate a sequent, if possible and leading to new facts.

frule Source

Arguments

:: MonadPlus m
=> Sequent	rule
-> Sequent	proof state
-> m (Mapping, Maybe Sequent)	some result if resolution worked. Nothing denotes that False was derived. Just means that premises of proof state were extended. mzero if rule could not be applied

Like fruleInst but tries all mappings.

fruleInst Source

Arguments

:: MonadPlus m
=> Sequent	rule
-> Mapping	mapping of free variables of rule to proof state
-> Sequent	proof state
-> m (Maybe Sequent)	some result if resolution worked. Nothing denotes that False was derived. Just means that premises of proof state were extended. mzero if rule could not be applied

Emulate a variant Isabelle's frule tactic. It works only if the given maping of free variables of the rule makes the premise of the rule provable under the given proof state. Then, the conclusion of the rule with free variables mapped accordingly is added to premises of the proof state. The last step works currently only for conclusions being false of pure conclusions.

NOTE that frule works only for rules that contain no existential quantifiers in the conclusion.

chainRule :: MonadPlus m => Sequent -> Message -> m [((String, [Either TID AgentId]), Sequent)]Source

Try to use the chain rule.

MonadPlus is used to report a failure to apply the rule.

splitEq :: MsgEq -> Sequent -> [Maybe Sequent]Source

Split a splittable equality. splitting can be done.

exploitTyping :: MonadPlus m => Sequent -> m Sequent Source

Try to exploit the typing. Fails if no new facts could be derived.

uniqueTIDQuantifiers :: Sequent -> Sequent Source

Make all thread identifiers occurring in the sequent unique by consistently relabeling the thread identifiers in the conclusion.