static int 
CommandBuildTrans(
  ClientData  clientData, 
  Tcl_Interp * interp, 
  int  argc, 
  char ** argv 
)
optional

Side Effects required

See Also optional
Defined in rtm.c

static int 
CommandComputeInitSet(
  ClientData  clientData, 
  Tcl_Interp * interp, 
  int  argc, 
  char ** argv 
)
Compute the mdd representing initial states of a module

Side Effects The initial region computed is added to the rtm region manager's region table

See Also CommandComputeReachedSet
Defined in rtm.c

static int 
CommandComputeReachSet(
  ClientData  clientData, 
  Tcl_Interp * interp, 
  int  argc, 
  char ** argv 
)
Compute reached set for a timed module using MDDs as the representation. The transition relation must be built using the command "rtm_trans" before this function is called

Side Effects The MDD representing the set of reached states is added to the rtmRegionTable associated with the module

Defined in rtm.c

static int 
CommandReadOrder(
  ClientData  clientData, 
  Tcl_Interp * interp, 
  int  argc, 
  char ** argv 
)
Read an ordering of MDD variables from a file, and order the MDD variables of a module accordingly

Side Effects none

See Also CommandWriteOrder
Defined in rtm.c

static int 
CommandRtmDynamicVarOrdering(
  ClientData  clientData, 
  Tcl_Interp * interp, 
  int  argc, 
  char ** argv 
)
Implements the rtm_dynamic_var_ordering command for the rtm package .

Defined in rtm.c

static void 
ModuleAssignMddIdsToVariables(
  Mdl_Module_t * module, 
  Sym_Info_t * symInfo, 
  array_t * totalVarArray 
)
Create MDD variables according to the specified total ordering

Side Effects MDD variables are created for each of the module variables, as specified by the total ordering SeeAlso [

Defined in rtm.c

static array_t * 
ModuleTotalOrderVariables(
  Mdl_Module_t * module, 
  array_t * varOrderArray 
)
Given a module and an array of variables (the order in which the variables are present in the array), pad remaining variables to the end of the array

Side Effects Remaining variables are added to the end of the array

See Also RtmReadOrder
Defined in rtm.c

void 
RtmCreateTimeIncVar(
  Rtm_Info_t * rtmInfo, 
  Mdl_Module_t * module 
)
optional

Side Effects required

See Also optional
Defined in rtm.c

static char * 
RtmDynOrderTypeConvertToString(
  bdd_reorder_type_t  method 
)
Converts a dynamic ordering method type to a string. This string must NOT be freed by the caller.

Defined in rtm.c

mdd_t * 
RtmGetMddLiteral(
  mdd_manager * manager, 
  int  id, 
  int  value 
)
optional

Side Effects required

See Also optional
Defined in rtmUtil.c

int 
RtmGetNvals(
  Rtm_Info_t * rtmInfo, 
  int  id 
)
optional

Side Effects required

See Also optional
Defined in rtm.c

int 
RtmGetTopMddId(
  mdd_t * m, 
  Rtm_Info_t * rtmInfo 
)
optional

Side Effects required

See Also optional
Defined in rtm.c

boolean 
RtmMddInTrueSupport(
  mdd_t * m, 
  int  id, 
  Rtm_Info_t * rtmInfo 
)
optional

Side Effects required

See Also optional
Defined in rtmUtil.c

mdd_t * 
RtmModuleSearch(
  Mdl_Module_t * module, 
  Rtm_Info_t * rtmInfo, 
  boolean  verbose, 
  boolean  checkInvariants, 
  array_t * invNameArray, 
  array_t * typedExprArray, 
  Tcl_Interp * interp 
)
reachability + optionally invariant checking on timed modules

Side Effects state of invariants may be changed

See Also Rtm_ModuleBuildTransitionRelation
Defined in rtm.c

array_t * 
RtmReadOrder(
  FILE * fp, 
  Mdl_Module_t * module 
)
Write variable order for module from a file

Side Effects none

See Also SymWriteOrder
Defined in rtm.c

static bdd_reorder_type_t 
RtmStringConvertToDynOrderType(
  char * string 
)
Converts a string to a dynamic ordering method type. If string is not "sift" or "window", then returns BDD_REORDER_NONE.

Defined in rtm.c

Rtm_Region_t * 
Rtm_AllocateRegionStruct(
  Mdl_Module_t * module, 
  mdd_t * regionSet 
)
optional

Side Effects required

See Also optional
Defined in rtm.c

mdd_t * 
Rtm_AssignmentsBuildMdd(
  Atm_Atom_t * atom, 
  Rtm_Info_t * rtmInfo, 
  Atm_Cmd_t * cmd 
)
builds the mdd for the assignments of a command

Side Effects none

See Also Rtm_AtomBuildTransitionRelation
Defined in rtm.c

void 
Rtm_AtomBuildInitCmdListMdds(
  Atm_Atom_t * atom, 
  Rtm_Info_t * rtmInfo, 
  mdd_t ** atomMddPtr, 
  mdd_t ** guardOrMddPtr 
)
updates mdds by processing the init commands of the atom guardOrMdd and atomMdd are affected.

Side Effects guardOrMdd and atomMdd are changed

See Also Rtm_AtomBuildInitialRegion
Defined in rtm.c

mdd_t * 
Rtm_AtomBuildInitialRegion(
  Atm_Atom_t * atom, 
  Rtm_Info_t * rtmInfo 
)
build initial region for an atom in a timed module

Side Effects none

See Also Rtm_AtomBuildTransitionRelation
Defined in rtm.c

mdd_t * 
Rtm_AtomBuildTransitionRelation(
  Atm_Atom_t * atom, 
  Rtm_Info_t * rtmInfo 
)
build transition relation for an atom One timed and one untimed conjunct is created for each atom The timed conjunct for the atom represents the transitions where one time unit elapses (all timers incremented by 1) The untimed conjunct for the atom represents control transitions where no time elapses. The first entry in the array returned is the timed conjunct, the second one is the untimed one.

Side Effects none

See Also Rtm_ModuleBuildTransitionRelation
Defined in rtm.c

void 
Rtm_AtomBuildUpdateCmdListMdds(
  Atm_Atom_t * atom, 
  Rtm_Info_t * rtmInfo, 
  mdd_t ** atomMddPtr, 
  mdd_t ** guardOrMddPtr 
)
updates mdds by processing the update commands of the atom guardOrMdd and atomMdd are affected.

Side Effects guardOrMdd and atomMdd are changed

See Also Rtm_AtomBuildTransitionRelation
Defined in rtm.c

void 
Rtm_AtomBuildWaitCmdListMdds(
  Atm_Atom_t * atom, 
  Rtm_Info_t * rtmInfo, 
  mdd_t ** atomMddPtr, 
  mdd_t ** timedGuardOrMddPtr 
)
updates mdds by processing the wait(delay) commands of the atom guardOrMdd and atomMdd are affected.

Side Effects guardOrMdd and atomMdd are changed

See Also Rtm_AtomBuildTransitionRelation
Defined in rtm.c

void 
Rtm_AtomProcessDefaultInitCommand(
  Atm_Atom_t * atom, 
  Rtm_Info_t * rtmInfo, 
  mdd_t ** atomMddPtr, 
  mdd_t ** guardOrMddPtr 
)
updates mdds by processing the default init command of the atom guardOrMdd and atomMdd are affected.

Side Effects guardOrMdd and atomMdd are changed

See Also Rtm_AtomBuildUpdateCmdListMdds Rtm_AtomBuildTransitionRelation
Defined in rtm.c

void 
Rtm_AtomProcessDefaultUpdateCommand(
  Atm_Atom_t * atom, 
  Rtm_Info_t * rtmInfo, 
  mdd_t ** atomMddPtr, 
  mdd_t ** guardOrMddPtr 
)
updates mdds by processing the default update command of the atom guardOrMdd and atomMdd are affected.

Side Effects guardOrMdd and atomMdd are changed

See Also Rtm_AtomBuildUpdateCmdListMdds Rtm_AtomBuildTransitionRelation
Defined in rtm.c

void 
Rtm_AtomProcessImplicitUpdateCommand(
  Atm_Atom_t * atom, 
  Rtm_Info_t * rtmInfo, 
  mdd_t ** atomMddPtr, 
  mdd_t ** guardOrMddPtr 
)
Process the implicit command for the update command list of an atom

Side Effects none

See Also Sym_AtomBuildTransitionRelation
Defined in rtm.c

mdd_t * 
Rtm_BuildOneWaitAssignmentMdd(
  Atm_Expr_t * expr, 
  Rtm_Info_t * rtmInfo, 
  int  pid, 
  int  uid 
)
builds the mdd for a single assignment of a wait command

Side Effects none

See Also Rtm_AtomBuildTransitionRelation
Defined in rtm.c

mdd_t * 
Rtm_BuildUnconstrainedTimerIncMdd(
  int  pid, 
  int  uid, 
  Var_Variable_t * var, 
  Rtm_Info_t * rtmInfo 
)
Timers not constrained by a wait command all increase by the amount "inc" as represented by the rtmInfo->timeIncId variable

Side Effects required

See Also optional
Defined in rtm.c

void 
Rtm_DebugTracePrint(
  Rtm_Info_t * rtmInfo, 
  array_t * savedOnions, 
  int  step, 
  mdd_t * notInv, 
  array_t * eventIdArray, 
  array_t * histDependIdArray, 
  char * invName, 
  char * moduleName, 
  Tcl_Interp * interp 
)
Given an array of MDDs (representing the onion ring), the step at which the error occured, the negation of the invariant that got violated, arrays of event and history free ids of the module, name of the invariant and module, this function prints the debug trace. It starts with the onion ring at the specified step and intersects it with the negation of the invariant. Then it successivey does pre-image computations and finds a path to an initial state. Then it reverses the path and and prints an error trace. It uses different displaying techniques if Tk interface is running

Side Effects none

See Also RtmModuleSearch
Defined in rtm.c

int 
Rtm_End(
  Tcl_Interp * interp, 
  Main_Manager_t * manager 
)
Currently this function does nothing. During a subsequent cleanup this should be made to free all memory allocated by the Rtm package.

Side Effects None

Defined in rtm.c

mdd_t * 
Rtm_GuardBuildMdd(
  Rtm_Info_t * rtmInfo, 
  Atm_Expr_t * guard 
)
builds the mdd for the guard of a command

Side Effects none

See Also Rtm_AtomBuildTransitionRelation
Defined in rtm.c

mdd_t * 
Rtm_InitAssignmentsBuildMdd(
  Atm_Atom_t * atom, 
  Rtm_Info_t * rtmInfo, 
  Atm_Cmd_t * cmd 
)
builds the mdd for the assignments of an init command

Side Effects none

See Also Rtm_AtomBuildTransitionRelation
Defined in rtm.c

int 
Rtm_Init(
  Tcl_Interp * interp, 
  Main_Manager_t * manager 
)
Registers the rtm package commands with tcl Allocates memory for RtmRegionManager and deposit it in the main manager.

Side Effects None

See Also Rtm_End Rtm_Reinit
Defined in rtm.c

mdd_t  * 
Rtm_MddPickMinterm(
  mdd_t * mdd, 
  Rtm_Info_t * rtmInfo 
)
optional

Side Effects required

See Also optional
Defined in rtm.c

void 
Rtm_MddPrintCubes(
  mdd_t * mdd, 
  Rtm_Info_t * rtmInfo, 
  int  level 
)
optional

Side Effects required

See Also optional
Defined in rtm.c

mdd_t * 
Rtm_ModuleBuildInitialRegion(
  Rtm_Info_t * rtmInfo, 
  Mdl_Module_t * module 
)
build mdd for initial region of module

Side Effects none

See Also Rtm_ModuleBuildTransitionRelation
Defined in rtm.c

void 
Rtm_ModuleBuildTransitionRelation(
  Rtm_Info_t * rtmInfo, 
  Mdl_Module_t * module 
)
build symbolic transition relation for a module. One timed and one untimed conjunct is created for each atom and timed and untimed conjuncts are stored in separate arrays The timed conjunct for the atom represents the transitions where one time unit elapses (all timers incremented by 1) The untimed conjunct for the atom represents control transitions where no time elapses.

Side Effects transition relation is built and stored in rtmInfo

See Also RtmModuleSearch
Defined in rtm.c

void 
Rtm_ModulePerformBFS(
  Tcl_Interp * interp, 
  Main_Manager_t * mainManager, 
  Mdl_Module_t * module, 
  array_t * invNameArray, 
  array_t * typedExprArray 
)
Do invariant checking. This is the entry point for the rtm invariant engine to be called from the inv package

Side Effects none

See Also Rtm_ModuleBuildTransitionRelation
Defined in rtm.c

void 
Rtm_RegionManagerAddModuleToRtmInfo(
  Rtm_RegionManager_t * rtmRegionManager, 
  Mdl_Module_t * module, 
  Rtm_Info_t * rtmInfo 
)
optional

Side Effects required

See Also optional
Defined in rtm.c

Rtm_RegionManager_t * 
Rtm_RegionManagerAlloc(
    
)
optional

Side Effects required

See Also optional
Defined in rtm.c

Rtm_Info_t * 
Rtm_RegionManagerObtainRtmInfoFromModule(
  Rtm_RegionManager_t * rtmRegionManager, 
  Mdl_Module_t * module 
)
optional

Side Effects required

See Also optional
Defined in rtm.c

Tcl_HashTable * 
Rtm_RegionManagerReadRegionTable(
  Rtm_RegionManager_t * rtmRegionManager 
)
optional

Side Effects required

See Also optional
Defined in rtm.c

int 
Rtm_Reinit(
  Tcl_Interp * interp, 
  Main_Manager_t * manager 
)
This function is called when the user types a re-init command. Re-initialization is not yet supported by Rtm. Currently, this function does nothing

Side Effects None

See Also Rtm_Init Rtm_End
Defined in rtm.c

unsigned long 
Rtm_RtmRegionManagerIncrementCounter(
  Rtm_RegionManager_t * rtmRegionManager 
)
optional

Side Effects required

See Also optional
Defined in rtm.c

unsigned long 
Rtm_RtmRegionManagerReadCounter(
  Rtm_RegionManager_t * rtmRegionManager 
)
optional

Side Effects required

See Also optional
Defined in rtm.c

mdd_t * 
Rtm_WaitAssignmentsBuildMdd(
  Atm_Atom_t * atom, 
  Rtm_Info_t * rtmInfo, 
  Atm_Cmd_t * cmd 
)
builds the mdd for all of the assignments of a wait command

Side Effects none

See Also Rtm_AtomBuildTransitionRelation
Defined in rtm.c

static int 
VarOrderIsInArray(
  array_t * varOrderArray, 
  VarOrder_t * varOrder 
)
check if a variable is in a varOrderArray

Side Effects none

Defined in rtm.c

Last updated on 980624 22h11