Evaluation (Averest)

Evaluation Module

Namespace: Averest.Simulation
Assembly: Averest.dll

This module implements data types and functions for the evaluation of expressions with respect of given variable environments. The result, as well as the variable environments may map the variables to values according to their types. To this end, scalar and compound types are distinguished, where scalar values are elements of the types that can be atomically written by actions. As a consequence, variables having a scalar type can be mapped additionally to one of the values Vbot and Vtop (see below).

Types

Type	Description
EnvUpdate	an EnvUpdate contains the information to write a value to a place in an environment that is specified by the QName an the ValuePointer list
Environment	Environment denotes the type for a variable environment that is a mapping from known variables to their values.
ScalarValue	ScalarValue defines the data type for scalar values that contain the values of the scalar data types and the two additional values Vbot and Vtop. Vbot means "yet unknown" and can be changed to a known value during causality analysis, and Vtop means "wrong value" which is the result of a erroneous evaluation such as negative nat subtraction, division by zero, negative logarithm, array bound errors, as well as write conflicts. The scalar values are partially ordered where Vbot is the minimal element, Vtop is the maximal element, and all other values are incomparable.
Value	Value defines the compound values, i.e., in addition to the scalar values that are added via the constructor Vscl, there are also tuples and arrays.
ValuePointer	Lists of ValuePointer values are used to address scalar values contained in a compound value.

Functions and values

Function or value	Description
`ConstExpr2ScalarValue expr` Full Usage: `ConstExpr2ScalarValue expr` Parameters: expr : `Expr` Returns: `ScalarValue`	convert constant expressions to scalar values expr : `Expr` Returns: `ScalarValue`
`ConstExpr2Value expr` Full Usage: `ConstExpr2Value expr` Parameters: expr : `Expr` Returns: `Value`	expr : `Expr` Returns: `Value`
`EnvGet env qn` Full Usage: `EnvGet env qn` Parameters: env : `Environment` qn : `QName` Returns: `Value`	(EnvGet env qn) determines the value to which variable name qn is mapped by env. An InternalException is thrown in case qn is not in the domain. env : `Environment` qn : `QName` Returns: `Value`
`EvalExpr envD envC expr` Full Usage: `EvalExpr envD envC expr` Parameters: envD : `Environment` envC : `Environment` expr : `Expr` Returns: `Value`	Given environments envD and envC for the discrete and continuous transitions, EvalExpr evaluates a given expression to a corresponding value. envD : `Environment` envC : `Environment` expr : `Expr` Returns: `Value`
`Infimum (x, y)` Full Usage: `Infimum (x, y)` Parameters: x : `Value` y : `Value` Returns: `Value`	compute the infimum of two compound values. x : `Value` y : `Value` Returns: `Value`
`InitialEnv decls` Full Usage: `InitialEnv decls` Parameters: decls : `Interface` Returns: `Environment`	Given a variable abbreviation list and a declaration list, InitialEnv computes the corresponding initial variable environment, i.e., that variable environment that maps all variables to values containing only Vbot. decls : `Interface` Returns: `Environment`
`LhsExpr2ValuePointer envD envC lhs` Full Usage: `LhsExpr2ValuePointer envD envC lhs` Parameters: envD : `Environment` envC : `Environment` lhs : `LhsExpr` Returns: `QName * ValuePointer list option`	LhsExpr2ValuePointer evaluates the LhsExpr lhs with environments envD,envC to a pair (qnLhs,qnPtr) where qnLhs is the name of the target variable of lhs, and qnPtr is a pointer where lhs refers to (in case qnPtr has a value). If qnPtr is None, the evaluation of the pointer contained an unknown value. Finally, the function may fail with an ExternalException if the evaluation resulted in a top value. envD : `Environment` envC : `Environment` lhs : `LhsExpr` Returns: `QName * ValuePointer list option`
`PrintHiddenFlag` Full Usage: `PrintHiddenFlag` Returns: `bool ref`	PrintHiddenFlag decides whether abbreviated variables of the AIF system are printed Returns: `bool ref`
`Printer` Full Usage: `Printer` Returns: `(Printer -> unit) ref`	Printer is a global variable that is used to print the output of the simulation. It is initialized with Prn2Print. Returns: `(Printer -> unit) ref`
`PrnEnv env` Full Usage: `PrnEnv env` Parameters: env : `Environment` Returns: `PrnDrv -> unit`	PrnEnv is a printer for environments (refer to Core.Printer for more info). It makes use of the global variables Printer and PrintHiddenFlag defined in this module. env : `Environment` Returns: `PrnDrv -> unit`
`ScalarInfimum (x, y)` Full Usage: `ScalarInfimum (x, y)` Parameters: x : `ScalarValue` y : `ScalarValue` Returns: `ScalarValue`	compute the infimum of two scalar values. x : `ScalarValue` y : `ScalarValue` Returns: `ScalarValue`
`ScalarSupremum (x, y)` Full Usage: `ScalarSupremum (x, y)` Parameters: x : `ScalarValue` y : `ScalarValue` Returns: `ScalarValue`	compute the supremum of two scalar values. x : `ScalarValue` y : `ScalarValue` Returns: `ScalarValue`
`Supremum (x, y)` Full Usage: `Supremum (x, y)` Parameters: x : `Value` y : `Value` Returns: `Value`	compute the supremum of two compound values. x : `Value` y : `Value` Returns: `Value`
`UpdateEnvByAsgnL env asL` Full Usage: `UpdateEnvByAsgnL env asL` Parameters: env : `Map<'a, Value>` asL : `('a * ValuePointer list * Value) list` Returns: `Map<'a, Value>`	UpdateEnvL updates a given environment env according to a list of triples (qn,ptr,qval): Given that that qn@ptr is evaluated by env to a qval', then the resulting variable environment will evaluate lhs to the supremum of qval and qval'. Hence, if qval' is Vbot, the resulting value of lhs is qval, if qval' is already qval, it remains so, and otherwise it will be Vtop. The updates in the list asL are done from left to right so that multiple writes in asL to the same lhs with different values will also result in value Vtop. env : `Map<'a, Value>` asL : `('a * ValuePointer list * Value) list` Returns: `Map<'a, Value>`
`UpdateEnvByEnv env1 env2` Full Usage: `UpdateEnvByEnv env1 env2` Parameters: env1 : `Environment` env2 : `Environment` Returns: `Map<QName, Value>`	(UpdateEnvByEnv env1 env2) overwrites environment env2 by environment env1, i.e., the resulting environment maps variables contained only in env2 to the value already given by env2, and variables occurring in env1 to the values given in env1 (thereby overwriting previous values of env2). env1 : `Environment` env2 : `Environment` Returns: `Map<QName, Value>`
`UpdateEnvByPtr env (qn, ptr, newval)` Full Usage: `UpdateEnvByPtr env (qn, ptr, newval)` Parameters: env : `Map<'a, Value>` qn : `'a` ptr : `ValuePointer list` newval : `Value` Returns: `Map<'a, Value>`	This function updates a given environment env by Value newval that is put at address pointer ptr of the value of the variable with name qn. The resulting variable environment will evaluate qn at address pointer ptr to the supremum of its previous value v and newval. Hence, if v is Vbot, the resulting value of lhs is newvalue, and if v is already newvalue, it remains so, and otherwise it will become Vtop. env : `Map<'a, Value>` qn : `'a` ptr : `ValuePointer list` newval : `Value` Returns: `Map<'a, Value>`
`containsScalarVal sc v` Full Usage: `containsScalarVal sc v` Parameters: sc : `ScalarValue` v : `Value` Returns: `bool`	check whether a compound value v contains a scalar value sc like Vbot sc : `ScalarValue` v : `Value` Returns: `bool`
`epsilon` Full Usage: `epsilon` Returns: `float ref`	Precision of numerical evaluations: real values are viewed as epsilon-spheres around the given real constant, i.e., comparisons of real-valued expressions are evaluated with an allowed inprecision of epsilon. For example: alpha == beta iff \|alpha - beta\| < epsilon. The variable is initialzed by 1.0e-50. Returns: `float ref`