tamarin-prover-theory-0.8.5.0: Term manipulation library for the tamarin prover.

PortabilityGHC only
MaintainerBenedikt Schmidt <beschmi@gmail.com>
Safe HaskellNone

Theory.Constraint.System.Guarded

Contents

Description

Guarded formulas.

Synopsis

Guarded formulas

data Guarded s c v Source

Constructors

GAto (Atom (VTerm c (BVar v))) 
GDisj (Disj (Guarded s c v)) 
GConj (Conj (Guarded s c v)) 
GGuarded Quantifier [s] [Atom (VTerm c (BVar v))] (Guarded s c v)

Denotes ALL xs. as => gf or Ex xs. as & gf& depending on the Quantifier. We assume that all bound variables xs occur in fi atoms in as.

Instances

Apply LNGuarded 
Foldable (Guarded s c) 
(Eq s, Eq c, Eq v) => Eq (Guarded s c v) 
(Ord s, Ord c, Ord v) => Ord (Guarded s c v) 
(Show s, Show c, Show v) => Show (Guarded s c v) 
(Binary s_1627723903, Binary c_1627723904, Binary v_1627723905) => Binary (Guarded s_1627723903 c_1627723904 v_1627723905) 
(NFData s_1627723903, NFData c_1627723904, NFData v_1627723905) => NFData (Guarded s_1627723903 c_1627723904 v_1627723905) 
Ord c => HasFrees (Guarded (String, LSort) c LVar) 

data GAtom t Source

Atoms that are allowed as guards.

Constructors

GEqE (t, t) 
GAction (t, Fact t) 

Instances

Eq t => Eq (GAtom t) 
Ord t => Ord (GAtom t) 
Show t => Show (GAtom t) 

Smart constructors

gfalse :: Guarded s c vSource

gfalse returns the guarded formula f with False - f.

gtrue :: Guarded s c vSource

gtrue returns the guarded formula f with True - f.

gdisj :: (Ord s, Ord c, Ord v) => [Guarded s c v] -> Guarded s c vSource

gdisj gfs smart constructor for the disjunction of gfs.

gconj :: (Ord s, Ord c, Ord v) => [Guarded s c v] -> Guarded s c vSource

gconj gfs smart constructor for the conjunction of gfs.

gex :: (Ord s, Ord c, Ord v) => [s] -> [Atom (VTerm c (BVar v))] -> Guarded s c v -> Guarded s c vSource

gall :: (Eq s, Eq c, Eq v) => [s] -> [Atom (VTerm c (BVar v))] -> Guarded s c v -> Guarded s c vSource

gnot :: (Ord s, Ord c, Ord v) => Guarded s c v -> Guarded s c vSource

Negate a guarded formula.

ginduct :: Ord c => LGuarded c -> Either String (LGuarded c, LGuarded c)Source

Try to prove the formula by applying induction over the trace. Returns Left errMsg if this is not possible. Returns a tuple of formulas: one formalizing the proof obligation of the base-case and one formalizing the proof obligation of the step-case.

formulaToGuarded :: HighlightDocument d => LNFormula -> Either d LNGuardedSource

formulaToGuarded fm returns a guarded formula gf that is equivalent to fm if possible.

formulaToGuarded_ :: LNFormula -> LNGuardedSource

formulaToGuarded fm returns a guarded formula gf that is equivalent to fm under the assumption that this is possible. If not, then error is called.

Transformation

simplifyGuardedSource

Arguments

:: (LNAtom -> Maybe Bool)

Partial assignment for truth value of atoms.

-> LNGuarded

Original formula

-> Maybe LNGuarded

Simplified formula, provided some simplification was performed.

Simplify a Guarded formula by replacing atoms with their truth value, if it can be determined.

mapGuardedAtoms :: (Integer -> Atom (VTerm c (BVar v)) -> Atom (VTerm d (BVar w))) -> Guarded s c v -> Guarded s d wSource

Map a guarded formula with scope info. The Integer argument denotes the number of quantifiers that have been encountered so far.

atomToGAtom :: Show t => Atom t -> GAtom tSource

Convert Atoms to GAtoms, if possible.

sortGAtoms :: [GAtom t] -> [GAtom t]Source

Stable sort that ensures that actions occur before equations.

Queries

isSafetyFormula :: HasFrees (Guarded s c v) => Guarded s c v -> BoolSource

Check whether the guarded formula is closed and does not contain an existential quantifier. This under-approximates the question whether the formula is a safety formula. A safety formula phi has the property that a trace violating it can never be extended to a trace satisfying it.

guardFactTags :: Guarded s c v -> [FactTag]Source

All FactTags that are used in guards.

Conversions to non-bound representations

bvarToLVar :: Ord c => Atom (VTerm c (BVar LVar)) -> Atom (VTerm c LVar)Source

Assuming that there are no more bound variables left in an atom of a formula, convert it to an atom with free variables only.

openGuarded :: (Ord c, MonadFresh m) => LGuarded c -> m (Maybe (Quantifier, [LVar], [Atom (VTerm c LVar)], LGuarded c))Source

openGuarded gf returns Just (qua,vs,ats,gf') if gf is a guarded clause and Nothing otherwise. In the first case, qua is the quantifier, vs is a list of fresh variables, ats is the antecedent, and gf' is the succedent. In both antecedent and succedent, the bound variables are replaced by vs.

Substitutions

substBound :: Ord c => [(Integer, LVar)] -> LGuarded c -> LGuarded cSource

substBound s gf substitutes each occurence of a bound variable i in dom(s) with the corresponding free variable s(i)=x in all atoms in gf.

substBoundAtom :: Ord c => [(Integer, LVar)] -> Atom (VTerm c (BVar LVar)) -> Atom (VTerm c (BVar LVar))Source

substBoundAtom s a substitutes each occurence of a bound variables i in dom(s) with the corresponding free variable x=s(i) in the atom a.

substFree :: Ord c => [(LVar, Integer)] -> LGuarded c -> LGuarded cSource

substFreeAtom s gf substitutes each occurence of a free variables v in dom(s) with the correpsonding bound variables i=s(v) in all atoms in gf.

substFreeAtom :: Ord c => [(LVar, Integer)] -> Atom (VTerm c (BVar LVar)) -> Atom (VTerm c (BVar LVar))Source

substFreeAtom s a substitutes each occurence of a free variables v in dom(s) with the bound variables i=s(v) in the atom a.

Pretty-printing

prettyGuardedSource

Arguments

:: HighlightDocument d 
=> LNGuarded

Guarded Formula.

-> d

Pretty printed formula.

Pretty print a formula.