Averest


Specifications Module

Types

Type Description

AcceptanceType

acceptance conditions for automata (FIN means finite words)

AutomatonSymb

DetAutomatonSymb

FixSign

defining least and greatest fixpoints

GetAtomFailure

OutputEqu

ProofGoal

SpecExpr

TransEqu

VerifTask

Functions and values

Function or value Description

AtomsInwards spec

Full Usage: AtomsInwards spec

Parameters:
Returns: SpecExpr

spec : SpecExpr
Returns: SpecExpr

AtomsOutwards spec

Full Usage: AtomsOutwards spec

Parameters:
Returns: SpecExpr

spec : SpecExpr
Returns: SpecExpr

FVarsProofGoal pg

Full Usage: FVarsProofGoal pg

Parameters:
Returns: Set<QName * QType>

pg : ProofGoal
Returns: Set<QName * QType>

FVarsSpecExpr specExpr

Full Usage: FVarsSpecExpr specExpr

Parameters:
Returns: Set<QName * QType>

specExpr : SpecExpr
Returns: Set<QName * QType>

False

Full Usage: False

Returns: BoolExpr

Returns: BoolExpr

IsCTL specExpr

Full Usage: IsCTL specExpr

Parameters:
Returns: bool

specExpr : SpecExpr
Returns: bool

IsExistentialLTL specExpr

Full Usage: IsExistentialLTL specExpr

Parameters:
Returns: bool

specExpr : SpecExpr
Returns: bool

IsMuCalculus specExpr

Full Usage: IsMuCalculus specExpr

Parameters:
Returns: bool

specExpr : SpecExpr
Returns: bool

IsPurePathFormula specExpr

Full Usage: IsPurePathFormula specExpr

Parameters:
Returns: bool

specExpr : SpecExpr
Returns: bool

IsUniversalLTL specExpr

Full Usage: IsUniversalLTL specExpr

Parameters:
Returns: bool

specExpr : SpecExpr
Returns: bool

MkAlways phi

Full Usage: MkAlways phi

Parameters:
Returns: SpecExpr

phi : SpecExpr
Returns: SpecExpr

MkEventual psi

Full Usage: MkEventual psi

Parameters:
Returns: SpecExpr

psi : SpecExpr
Returns: SpecExpr

MkListSpecConj eL

Full Usage: MkListSpecConj eL

Parameters:
Returns: SpecExpr

eL : seq<SpecExpr>
Returns: SpecExpr

MkListSpecDisj eL

Full Usage: MkListSpecDisj eL

Parameters:
Returns: SpecExpr

eL : seq<SpecExpr>
Returns: SpecExpr

MkNext phi

Full Usage: MkNext phi

Parameters:
Returns: SpecExpr

phi : SpecExpr
Returns: SpecExpr

MkSpecConj (arg1, arg2)

Full Usage: MkSpecConj (arg1, arg2)

Parameters:
Returns: SpecExpr

arg0 : SpecExpr
arg1 : SpecExpr
Returns: SpecExpr

MkSpecDisj (arg1, arg2)

Full Usage: MkSpecDisj (arg1, arg2)

Parameters:
Returns: SpecExpr

arg0 : SpecExpr
arg1 : SpecExpr
Returns: SpecExpr

MkSpecEqv (arg1, arg2)

Full Usage: MkSpecEqv (arg1, arg2)

Parameters:
Returns: SpecExpr

arg0 : SpecExpr
arg1 : SpecExpr
Returns: SpecExpr

MkSpecImpl (arg1, arg2)

Full Usage: MkSpecImpl (arg1, arg2)

Parameters:
Returns: SpecExpr

arg0 : SpecExpr
arg1 : SpecExpr
Returns: SpecExpr

MkSpecNeg spec

Full Usage: MkSpecNeg spec

Parameters:
Returns: SpecExpr

spec : SpecExpr
Returns: SpecExpr

MkStrongBefore (phi, psi)

Full Usage: MkStrongBefore (phi, psi)

Parameters:
Returns: SpecExpr

phi : SpecExpr
psi : SpecExpr
Returns: SpecExpr

MkStrongUntil (phi, psi)

Full Usage: MkStrongUntil (phi, psi)

Parameters:
Returns: SpecExpr

phi : SpecExpr
psi : SpecExpr
Returns: SpecExpr

MkStrongWhen (phi, psi)

Full Usage: MkStrongWhen (phi, psi)

Parameters:
Returns: SpecExpr

phi : SpecExpr
psi : SpecExpr
Returns: SpecExpr

MkWeakBefore (phi, psi)

Full Usage: MkWeakBefore (phi, psi)

Parameters:
Returns: SpecExpr

phi : SpecExpr
psi : SpecExpr
Returns: SpecExpr

MkWeakUntil (phi, psi)

Full Usage: MkWeakUntil (phi, psi)

Parameters:
Returns: SpecExpr

phi : SpecExpr
psi : SpecExpr
Returns: SpecExpr

MkWeakWhen (phi, psi)

Full Usage: MkWeakWhen (phi, psi)

Parameters:
Returns: SpecExpr

phi : SpecExpr
psi : SpecExpr
Returns: SpecExpr

NNF neg specExpr

Full Usage: NNF neg specExpr

Parameters:
Returns: SpecExpr

neg : bool
specExpr : SpecExpr
Returns: SpecExpr

PrnProofGoal x

Full Usage: PrnProofGoal x

Parameters:
Returns: PrnDrv -> unit

x : ProofGoal
Returns: PrnDrv -> unit

PrnSpecExpr e

Full Usage: PrnSpecExpr e

Parameters:
Returns: PrnDrv -> unit

e : SpecExpr
Returns: PrnDrv -> unit

PrnVerifTask x

Full Usage: PrnVerifTask x

Parameters:
Returns: PrnDrv -> unit

x : VerifTask
Returns: PrnDrv -> unit

SortSpecExprPair (t1, t2)

Full Usage: SortSpecExprPair (t1, t2)

Parameters:
    t1 : 'a
    t2 : 'a

Returns: 'a * 'a

t1 : 'a
t2 : 'a
Returns: 'a * 'a

SubstAtoms rho specExpr

Full Usage: SubstAtoms rho specExpr

Parameters:
Returns: SpecExpr

rho : Map<QName, Expr>
specExpr : SpecExpr
Returns: SpecExpr

SubstProofGoal rho proofGoal

Full Usage: SubstProofGoal rho proofGoal

Parameters:
Returns: ProofGoal

rho : Map<QName, Expr>
proofGoal : ProofGoal
Returns: ProofGoal

SubstSpecExpr rho phi

Full Usage: SubstSpecExpr rho phi

Parameters:
Returns: SpecExpr

rho : Map<QName, SpecExpr>
phi : SpecExpr
Returns: SpecExpr

TempLogicExpr2Latex phi

Full Usage: TempLogicExpr2Latex phi

Parameters:
Returns: string

print a CTL* formula in Latex

phi : SpecExpr
Returns: string

True

Full Usage: True

Returns: BoolExpr

Returns: BoolExpr

VectorMu2FlatMu specExpr

Full Usage: VectorMu2FlatMu specExpr

Parameters:
Returns: SpecExpr

specExpr : SpecExpr
Returns: SpecExpr