Module dev.civl.mc

Package dev.civl.mc.model.IF.type

Interface CIVLStateType

All Superinterfaces:

CIVLPrimitiveType, CIVLType

public interface CIVLStateType
extends CIVLPrimitiveType

Nested Class Summary

Nested classes/interfaces inherited from interface dev.civl.mc.model.IF.type.CIVLPrimitiveType

CIVLPrimitiveType.PrimitiveTypeKind

Nested classes/interfaces inherited from interface dev.civl.mc.model.IF.type.CIVLType

CIVLType.TypeKind

Method Summary

Modifier and Type	Method	Description
dev.civl.sarl.IF.expr.SymbolicExpression	buildStateValue(dev.civl.sarl.IF.SymbolicUniverse universe, int stateKey, dev.civl.sarl.IF.expr.SymbolicExpression scopeValuesToReal)	Translate an integer canonical state id into a symbolic expression
dev.civl.sarl.IF.expr.SymbolicExpression	selectScopeValuesMap(dev.civl.sarl.IF.SymbolicUniverse universe, dev.civl.sarl.IF.expr.SymbolicExpression stateValue)	Extract the scope value mapper from an object of the CIVLStateType.
int	selectStateKey(dev.civl.sarl.IF.SymbolicUniverse universe, dev.civl.sarl.IF.expr.SymbolicExpression stateValue)	Extracts the integral key from an object of CIVLStateType.

Methods inherited from interface dev.civl.mc.model.IF.type.CIVLPrimitiveType

getFacts, getSizeof, primitiveTypeKind

Methods inherited from interface dev.civl.mc.model.IF.type.CIVLType

analyze, areSubtypesScalar, copyAs, freeVariables, getDynamicType, getDynamicTypeIndex, getStateVariable, hasReferences, hasState, isArrayType, isBoolType, isBundleType, isCharType, isDomainType, isEnumerationType, isFunction, isHeapType, isIncompleteArrayType, isIntegerType, isNumericType, isPointerType, isProcessType, isRangeType, isRealType, isScalar, isScopeType, isSetType, isSetTypeOf, isStructType, isSuperTypeOf, isUnionType, isVoidType, setStateVariable, typeKind

Method Details

selectScopeValuesMap

dev.civl.sarl.IF.expr.SymbolicExpression selectScopeValuesMap(dev.civl.sarl.IF.SymbolicUniverse universe,
 dev.civl.sarl.IF.expr.SymbolicExpression stateValue)

Extract the scope value mapper from an object of the CIVLStateType. A scope value mapper is an array where indices are integral keys of scope values of the state represented by the object and indexed elements are corresponding scope values in the current state.

Parameters:

universe - a reference to SymbolicUniverse

stateValue - the value of an object of CIVLStateType

Returns:

the integer array which maps scope values in the state value to scope values in the current state.

selectStateKey

int selectStateKey(dev.civl.sarl.IF.SymbolicUniverse universe,
 dev.civl.sarl.IF.expr.SymbolicExpression stateValue)

Extracts the integral key from an object of CIVLStateType.

Parameters:

universe - a reference to SymbolicUniverse

stateValue - the value of an object of CIVLStateType

Returns:

a unique integral key value which identifies the state value

buildStateValue

dev.civl.sarl.IF.expr.SymbolicExpression buildStateValue(dev.civl.sarl.IF.SymbolicUniverse universe,
 int stateKey,
 dev.civl.sarl.IF.expr.SymbolicExpression scopeValuesToReal)

Translate an integer canonical state id into a symbolic expression

Parameters:

universe - a reference to SymbolicUniverse

stateKey - The integer identifier of the generating state value

scopeValuesToReal - an integer array that maps scope values in the state value to scope values in the real state.

Returns:

The symbolic expression representing a state