rtm.h
External header file
rtmInt.h
Internal header file
rtm.c
rtmUtil.c

rtm.h

External header file

By: Serdar Tasiran


rtmInt.h

Internal header file

By: Serdar Tasiran


rtm.c

By: Serdar Tasiran

Rtm_Init()
Initializes the rtm package
Rtm_Reinit()
Re-initializes the rtm package
Rtm_End()
Closes the rtm package
Rtm_ModulePerformBFS()
do invariant checking on a timed module
Rtm_ModuleBuildTransitionRelation()
build transition relation (as an MDD) for a timed module
Rtm_AtomBuildTransitionRelation()
build transition relation for an atom
Rtm_AtomBuildUpdateCmdListMdds()
updates mdds by processing the update commands of the atom
Rtm_AtomBuildWaitCmdListMdds()
updates mdds by processing the wait(delay) commands of the atom
Rtm_GuardBuildMdd()
builds the mdd for the guard of a command
Rtm_AssignmentsBuildMdd()
builds the mdd for the assignments of a command
Rtm_InitAssignmentsBuildMdd()
builds the mdd for the assignments of an init command
Rtm_AtomProcessDefaultUpdateCommand()
updates mdds by processing the default update command of the atom
Rtm_AtomProcessImplicitUpdateCommand()
Process the implicit command for the update command list of an atom
Rtm_WaitAssignmentsBuildMdd()
builds the mdd for all of the assignments of a wait command
Rtm_BuildOneWaitAssignmentMdd()
builds the mdd for a single assignment of a wait command
Rtm_BuildUnconstrainedTimerIncMdd()
Builds the mdd for timers not constrained by a wait command
RtmReadOrder()
Read variable order for module from a file
RtmCreateTimeIncVar()
required
Rtm_RegionManagerReadRegionTable()
required
Rtm_RegionManagerObtainRtmInfoFromModule()
required
Rtm_RegionManagerAlloc()
required
Rtm_RegionManagerAddModuleToRtmInfo()
required
Rtm_ModuleBuildInitialRegion()
build mdd for initial region of module
Rtm_AtomBuildInitialRegion()
build initial region for an atom in a timed module
Rtm_AtomBuildInitCmdListMdds()
updates mdds by processing the init commands of the atom
Rtm_AtomProcessDefaultInitCommand()
updates mdds by processing the default init command of the atom
Rtm_AllocateRegionStruct()
required
Rtm_RtmRegionManagerReadCounter()
required
Rtm_RtmRegionManagerIncrementCounter()
required
Rtm_MddPrintCubes()
required
RtmGetNvals()
required
RtmGetTopMddId()
required
RtmModuleSearch()
do reachability + invariant checking on timed modules
Rtm_DebugTracePrint()
print debug trace for an invariant for timed modules
Rtm_MddPickMinterm()
required
CommandReadOrder()
Order the MDD variables of a module as specified by a file
CommandComputeReachSet()
Computes the reached state set of a timed module
CommandComputeInitSet()
driver for building initial state of a timed module
CommandBuildTrans()
required
RtmStringConvertToDynOrderType()
Converts a string to a dynamic ordering method type.
RtmDynOrderTypeConvertToString()
Converts a dynamic ordering method type to a string.
CommandRtmDynamicVarOrdering()
Implements the rtm_dynamic_var_ordering command for the rtm package .
ModuleTotalOrderVariables()
Convert an ordering of a subset of variables to a total ordering
VarOrderIsInArray()
check if a variable is in a varOrderArray
ModuleAssignMddIdsToVariables()
Create MDD variables according to the specified total ordering

rtmUtil.c

By: Serdar Tasiran

RtmMddInTrueSupport()
Check if the given variable is in the true support of the given mdd
RtmGetMddLiteral()
utility to get and MDD literal

Last updated on 980624 22h11