Properties (Averest)

Properties Module

Namespace: Averest.Transform
Assembly: Averest.dll

This file implements ...

Types

Type	Description
SystemPartProperty
SystemProperty

Functions and values

Function or value	Description
`AIFInvariants` Full Usage: `AIFInvariants` Returns: `SystemProperty list`	invariants holding for well-typed AIF files Returns: `SystemProperty list`
`AbbrevsEmpty` Full Usage: `AbbrevsEmpty` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`AbsReactionEmpty` Full Usage: `AbsReactionEmpty` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`AbsReactsAreUnique` Full Usage: `AbsReactsAreUnique` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`AbsReactsInputFree` Full Usage: `AbsReactsInputFree` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`AbsReactsLabelFree` Full Usage: `AbsReactsLabelFree` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`AbsReactsOnlyCells` Full Usage: `AbsReactsOnlyCells` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`AbsReactsOutputReadFree` Full Usage: `AbsReactsOutputReadFree` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`ActionsOutputReadFree` Full Usage: `ActionsOutputReadFree` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`AssignedVariablesAreDeclared` Full Usage: `AssignedVariablesAreDeclared` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`CheckDrivers pred system` Full Usage: `CheckDrivers pred system` Parameters: pred : `Interface -> SystemPart -> bool` system : `AIFSystem` Returns: `bool`	pred : `Interface -> SystemPart -> bool` system : `AIFSystem` Returns: `bool`
`CheckMainSystemPart pred system` Full Usage: `CheckMainSystemPart pred system` Parameters: pred : `Interface -> SystemPart -> bool` system : `AIFSystem` Returns: `bool`	pred : `Interface -> SystemPart -> bool` system : `AIFSystem` Returns: `bool`
`CheckObservers pred system` Full Usage: `CheckObservers pred system` Parameters: pred : `Interface -> SystemPart -> bool` system : `AIFSystem` Returns: `bool`	pred : `Interface -> SystemPart -> bool` system : `AIFSystem` Returns: `bool`
`CheckPostconditions name props system` Full Usage: `CheckPostconditions name props system` Parameters: name : `string` props : `SystemProperty list` system : `AIFSystem`	Checks a list of postconditions for a given system name : `string` props : `SystemProperty list` system : `AIFSystem`
`CheckPreconditions name props system` Full Usage: `CheckPreconditions name props system` Parameters: name : `string` props : `SystemProperty list` system : `AIFSystem`	Checks a list of preconditions for a given system. name : `string` props : `SystemProperty list` system : `AIFSystem`
`CheckPreservations name props oldSystem newSystem` Full Usage: `CheckPreservations name props oldSystem newSystem` Parameters: name : `string` props : `SystemProperty list` oldSystem : `AIFSystem` newSystem : `AIFSystem`	Checks a list of preservation conditions for a system given before and after a certain transformation name : `string` props : `SystemProperty list` oldSystem : `AIFSystem` newSystem : `AIFSystem`
`CheckSystemParts pred system` Full Usage: `CheckSystemParts pred system` Parameters: pred : `Interface -> SystemPart -> bool` system : `AIFSystem` Returns: `bool`	pred : `Interface -> SystemPart -> bool` system : `AIFSystem` Returns: `bool`
`CtrlEmpty` Full Usage: `CtrlEmpty` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`CtrlNowFree` Full Usage: `CtrlNowFree` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`CtrlOnlyLabelsAssigned` Full Usage: `CtrlOnlyLabelsAssigned` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`DataInputAssignFree` Full Usage: `DataInputAssignFree` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`DataLabelAssignFree` Full Usage: `DataLabelAssignFree` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`DataLabelsOnlyReadInGuards` Full Usage: `DataLabelsOnlyReadInGuards` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`DataNowFree` Full Usage: `DataNowFree` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`DataNxtEventFree` Full Usage: `DataNxtEventFree` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`DataNxtFree` Full Usage: `DataNxtFree` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`DeclsInOutFree` Full Usage: `DeclsInOutFree` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`DeclsInputFree` Full Usage: `DeclsInputFree` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`DeclsOutputFree` Full Usage: `DeclsOutputFree` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`DriverInterface iface` Full Usage: `DriverInterface iface` Parameters: iface : `('a * Decl) list` Returns: `('a * Decl) list`	iface : `('a * Decl) list` Returns: `('a * Decl) list`
`GetDriverSystemParts system` Full Usage: `GetDriverSystemParts system` Parameters: system : `AIFSystem` Returns: `SystemPart list`	system : `AIFSystem` Returns: `SystemPart list`
`GetObserverSystemParts system` Full Usage: `GetObserverSystemParts system` Parameters: system : `AIFSystem` Returns: `SystemPart list`	system : `AIFSystem` Returns: `SystemPart list`
`InterfaceLabelFree` Full Usage: `InterfaceLabelFree` Returns: `SystemProperty`	Returns: `SystemProperty`
`InterfaceLocVarFree` Full Usage: `InterfaceLocVarFree` Returns: `SystemProperty`	Returns: `SystemProperty`
`IsCell lhsExpr` Full Usage: `IsCell lhsExpr` Parameters: lhsExpr : `LhsExpr` Returns: `bool`	lhsExpr : `LhsExpr` Returns: `bool`
`LabelsAreEvent` Full Usage: `LabelsAreEvent` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`ObserverInterface iface` Full Usage: `ObserverInterface iface` Parameters: iface : `('a * Decl) list` Returns: `('a * Decl) list`	iface : `('a * Decl) list` Returns: `('a * Decl) list`
`OnlyCellsWritten` Full Usage: `OnlyCellsWritten` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`OnlyScalars` Full Usage: `OnlyScalars` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`OutputsNxtFree` Full Usage: `OutputsNxtFree` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`SystemPartProp2SystemProp partProp` Full Usage: `SystemPartProp2SystemProp partProp` Parameters: partProp : `SystemPartProperty` Returns: `SystemProperty`	partProp : `SystemPartProperty` Returns: `SystemProperty`
`VarsDeclaredOnce` Full Usage: `VarsDeclaredOnce` Returns: `SystemPartProperty`	Returns: `SystemPartProperty`
`isGrdAssign (arg1, act)` Full Usage: `isGrdAssign (arg1, act)` Parameters: arg0 : `'a` act : `Action` Returns: `bool`	arg0 : `'a` act : `Action` Returns: `bool`
`isGrdAssignNow (arg1, act)` Full Usage: `isGrdAssignNow (arg1, act)` Parameters: arg0 : `'a` act : `Action` Returns: `bool`	arg0 : `'a` act : `Action` Returns: `bool`
`isGrdAssignNxt (arg1, act)` Full Usage: `isGrdAssignNxt (arg1, act)` Parameters: arg0 : `'a` act : `Action` Returns: `bool`	arg0 : `'a` act : `Action` Returns: `bool`