Specifications (Averest)

Specifications Module

Namespace: Averest.Core
Assembly: Averest.dll

Types

Type	Description
DetAutoTuple
FixSign
GetAtomFailure
'a NDetAutoTuple
ProofGoal
SpecExpr
StateTransEq
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`
`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`
`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`
`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`
`True` Full Usage: `True` Returns: `BoolExpr`	Returns: `BoolExpr`
`VectorMu2FlatMu specExpr` Full Usage: `VectorMu2FlatMu specExpr` Parameters: specExpr : `SpecExpr` Returns: `SpecExpr`	specExpr : `SpecExpr` Returns: `SpecExpr`