Package edu.udel.cis.vsl.civl.kripke.IF

Interface LibraryEnabler

public interface LibraryEnabler

A Library Enabler provides a method to compute the enabled transitions of system function calls at a certain state for a give process. It also provides a method to compute the ample set of processes at a given state for a given process. A new library is implemented in the package named as "edu.udel.cis.vsl.civl.library." ( CIVLConstants.LIBRARY_PREFIX) + library name. And the class name of the enabler is: "Lib" + library name + "Enabler". For example, the stdio library enabler is implemented as the class edu.udel.cis.vsl.civl.library.stdio.LibstdioEnabler.

Method Summary

Modifier and Type	Method	Description
java.util.BitSet	ampleSet(State state, int pid, CallOrSpawnStatement statement, MemoryUnitSet[] setsReachableRead, MemoryUnitSet[] setsReachableWrite)	Computes the ample set process IDs from a system function call at a given state for a given process.
java.util.List<Transition>	enabledTransitions(State state, CallOrSpawnStatement call, edu.udel.cis.vsl.sarl.IF.expr.BooleanExpression pathCondition, int pid, Transition.AtomicLockAction atomicLockAction)	Computes the enabled transitions of a given function call.

Method Detail

ampleSet

java.util.BitSet ampleSet(State state,
                          int pid,
                          CallOrSpawnStatement statement,
                          MemoryUnitSet[] setsReachableRead,
                          MemoryUnitSet[] setsReachableWrite)
                   throws UnsatisfiablePathConditionException

Computes the ample set process IDs from a system function call at a given state for a given process.

Precondition: the call statement is enabled at the given state and it is one of the outgoing statements of process pid.

Contract: nothing dependent on the given statement can occur without one of the transitions of the processes in the returned ample set occurring first.

Parameters:

state - The current state.

pid - The ID of the process that the system function call belongs to.

statement - The system function call statement.

reachablePtrWritableMap -

reachablePtrReadonlyMap -

reachableNonPtrWritableMap -

reachableNonPtrReadonlyMap -

reachableMemUnitsMap - The map of reachable memory units of all active processes.

Returns:

the ample set of process IDs

Throws:

UnsatisfiablePathConditionException

enabledTransitions

java.util.List<Transition> enabledTransitions(State state,
                                              CallOrSpawnStatement call,
                                              edu.udel.cis.vsl.sarl.IF.expr.BooleanExpression pathCondition,
                                              int pid,
                                              Transition.AtomicLockAction atomicLockAction)
                                       throws UnsatisfiablePathConditionException

Computes the enabled transitions of a given function call. This is to support nondeterministic function calls.

Parameters:

state - The current state.

call - The function call statement, upon which the set of enabled transitions will be computed.

pathCondition - The current path condition.

pid - The ID of the process that the function call belongs to.

atomicLockAction - The action for the atomic lock variable, could be NONE, GRAB, or RELEASE. see also Transition.AtomicLockAction.

Returns:

The set of enabled transitions.

Throws:

UnsatisfiablePathConditionException