Specifications (Averest)

Specifications Module

Namespace: Averest.Core
Assembly: Averest.dll

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: spec : `SpecExpr` Returns: `SpecExpr`	spec : `SpecExpr` Returns: `SpecExpr`
`AtomsOutwards spec` Full Usage: `AtomsOutwards spec` Parameters: spec : `SpecExpr` Returns: `SpecExpr`	spec : `SpecExpr` Returns: `SpecExpr`
`FVarsProofGoal pg` Full Usage: `FVarsProofGoal pg` Parameters: pg : `ProofGoal` Returns: `Set<QName * QType>`	pg : `ProofGoal` Returns: `Set<QName * QType>`
`FVarsSpecExpr specExpr` Full Usage: `FVarsSpecExpr specExpr` Parameters: specExpr : `SpecExpr` 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: specExpr : `SpecExpr` Returns: `bool`	specExpr : `SpecExpr` Returns: `bool`
`IsExistentialLTL specExpr` Full Usage: `IsExistentialLTL specExpr` Parameters: specExpr : `SpecExpr` Returns: `bool`	specExpr : `SpecExpr` Returns: `bool`
`IsMuCalculus specExpr` Full Usage: `IsMuCalculus specExpr` Parameters: specExpr : `SpecExpr` Returns: `bool`	specExpr : `SpecExpr` Returns: `bool`
`IsPurePathFormula specExpr` Full Usage: `IsPurePathFormula specExpr` Parameters: specExpr : `SpecExpr` Returns: `bool`	specExpr : `SpecExpr` Returns: `bool`
`IsUniversalLTL specExpr` Full Usage: `IsUniversalLTL specExpr` Parameters: specExpr : `SpecExpr` Returns: `bool`	specExpr : `SpecExpr` Returns: `bool`
`MkAlways phi` Full Usage: `MkAlways phi` Parameters: phi : `SpecExpr` Returns: `SpecExpr`	phi : `SpecExpr` Returns: `SpecExpr`
`MkEventual psi` Full Usage: `MkEventual psi` Parameters: psi : `SpecExpr` Returns: `SpecExpr`	psi : `SpecExpr` Returns: `SpecExpr`
`MkListSpecConj eL` Full Usage: `MkListSpecConj eL` Parameters: eL : `seq<SpecExpr>` Returns: `SpecExpr`	eL : `seq<SpecExpr>` Returns: `SpecExpr`
`MkListSpecDisj eL` Full Usage: `MkListSpecDisj eL` Parameters: eL : `seq<SpecExpr>` Returns: `SpecExpr`	eL : `seq<SpecExpr>` Returns: `SpecExpr`
`MkNext phi` Full Usage: `MkNext phi` Parameters: phi : `SpecExpr` Returns: `SpecExpr`	phi : `SpecExpr` Returns: `SpecExpr`
`MkSpecConj (arg1, arg2)` Full Usage: `MkSpecConj (arg1, arg2)` Parameters: arg0 : `SpecExpr` arg1 : `SpecExpr` Returns: `SpecExpr`	arg0 : `SpecExpr` arg1 : `SpecExpr` Returns: `SpecExpr`
`MkSpecDisj (arg1, arg2)` Full Usage: `MkSpecDisj (arg1, arg2)` Parameters: arg0 : `SpecExpr` arg1 : `SpecExpr` Returns: `SpecExpr`	arg0 : `SpecExpr` arg1 : `SpecExpr` Returns: `SpecExpr`
`MkSpecEqv (arg1, arg2)` Full Usage: `MkSpecEqv (arg1, arg2)` Parameters: arg0 : `SpecExpr` arg1 : `SpecExpr` Returns: `SpecExpr`	arg0 : `SpecExpr` arg1 : `SpecExpr` Returns: `SpecExpr`
`MkSpecImpl (arg1, arg2)` Full Usage: `MkSpecImpl (arg1, arg2)` Parameters: arg0 : `SpecExpr` arg1 : `SpecExpr` Returns: `SpecExpr`	arg0 : `SpecExpr` arg1 : `SpecExpr` Returns: `SpecExpr`
`MkSpecNeg spec` Full Usage: `MkSpecNeg spec` Parameters: spec : `SpecExpr` Returns: `SpecExpr`	spec : `SpecExpr` Returns: `SpecExpr`
`MkStrongBefore (phi, psi)` Full Usage: `MkStrongBefore (phi, psi)` Parameters: phi : `SpecExpr` psi : `SpecExpr` Returns: `SpecExpr`	phi : `SpecExpr` psi : `SpecExpr` Returns: `SpecExpr`
`MkStrongUntil (phi, psi)` Full Usage: `MkStrongUntil (phi, psi)` Parameters: phi : `SpecExpr` psi : `SpecExpr` Returns: `SpecExpr`	phi : `SpecExpr` psi : `SpecExpr` Returns: `SpecExpr`
`MkStrongWhen (phi, psi)` Full Usage: `MkStrongWhen (phi, psi)` Parameters: phi : `SpecExpr` psi : `SpecExpr` Returns: `SpecExpr`	phi : `SpecExpr` psi : `SpecExpr` Returns: `SpecExpr`
`MkWeakBefore (phi, psi)` Full Usage: `MkWeakBefore (phi, psi)` Parameters: phi : `SpecExpr` psi : `SpecExpr` Returns: `SpecExpr`	phi : `SpecExpr` psi : `SpecExpr` Returns: `SpecExpr`
`MkWeakUntil (phi, psi)` Full Usage: `MkWeakUntil (phi, psi)` Parameters: phi : `SpecExpr` psi : `SpecExpr` Returns: `SpecExpr`	phi : `SpecExpr` psi : `SpecExpr` Returns: `SpecExpr`
`MkWeakWhen (phi, psi)` Full Usage: `MkWeakWhen (phi, psi)` Parameters: phi : `SpecExpr` psi : `SpecExpr` Returns: `SpecExpr`	phi : `SpecExpr` psi : `SpecExpr` Returns: `SpecExpr`
`NNF neg specExpr` Full Usage: `NNF neg specExpr` Parameters: neg : `bool` specExpr : `SpecExpr` Returns: `SpecExpr`	neg : `bool` specExpr : `SpecExpr` Returns: `SpecExpr`
`PrnProofGoal x` Full Usage: `PrnProofGoal x` Parameters: x : `ProofGoal` Returns: `PrnDrv -> unit`	x : `ProofGoal` Returns: `PrnDrv -> unit`
`PrnSpecExpr e` Full Usage: `PrnSpecExpr e` Parameters: e : `SpecExpr` Returns: `PrnDrv -> unit`	e : `SpecExpr` Returns: `PrnDrv -> unit`
`PrnVerifTask x` Full Usage: `PrnVerifTask x` Parameters: x : `VerifTask` 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: rho : `Map<QName, Expr>` specExpr : `SpecExpr` Returns: `SpecExpr`	rho : `Map<QName, Expr>` specExpr : `SpecExpr` Returns: `SpecExpr`
`SubstProofGoal rho proofGoal` Full Usage: `SubstProofGoal rho proofGoal` Parameters: rho : `Map<QName, Expr>` proofGoal : `ProofGoal` Returns: `ProofGoal`	rho : `Map<QName, Expr>` proofGoal : `ProofGoal` Returns: `ProofGoal`
`SubstSpecExpr rho phi` Full Usage: `SubstSpecExpr rho phi` Parameters: rho : `Map<QName, SpecExpr>` phi : `SpecExpr` Returns: `SpecExpr`	rho : `Map<QName, SpecExpr>` phi : `SpecExpr` Returns: `SpecExpr`
`TempLogicExpr2Latex phi` Full Usage: `TempLogicExpr2Latex phi` Parameters: phi : `SpecExpr` 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: specExpr : `SpecExpr` Returns: `SpecExpr`	specExpr : `SpecExpr` Returns: `SpecExpr`