void 
BddFsmCache_copy_reachables(
  BddFsmCache_ptr  self, 
  const BddFsmCache_ptr  other 
)
This method is used when copying reachable states information between to FSMs

Defined in BddFsmCache.c

BddFsmCache_ptr 
BddFsmCache_create(
  DdManager* dd 
)
Class contructor

Defined in BddFsmCache.c

void 
BddFsmCache_destroy(
  BddFsmCache_ptr  self 
)
Class destructor

Defined in BddFsmCache.c

BddFsmCache_ptr 
BddFsmCache_hard_copy(
  const BddFsmCache_ptr  self 
)
Hardly copy the instance, by creating a new, separate family

See Also BddFsmCache_soft_copy
Defined in BddFsmCache.c

void 
BddFsmCache_reset_not_reusable_fields_after_product(
  BddFsmCache_ptr  self 
)
This is called when syncronous product is carried out. In particular LTL BDD-based model checking, after having applied the product between the original fsm and the fsm coming from the tableau contruction, needs to disable the cache sharing and to recalculate fair states and other fields, since the fsm changed. All fsm's fields that need to be recalculated after the syncronous product must be reset by this method.

See Also BddFsm_apply_synchronous_product
Defined in BddFsmCache.c

void 
BddFsmCache_set_reachables(
  BddFsmCache_ptr  self, 
  BddStates  states, 
  node_ptr  layers_list, 
  const int  diameter 
)
Given list layers_list must be reversed, from last layer to the layer corresponding to initial state. Given list layers_list will be destroyed.

Side Effects given list layers_list will be destroyed, cache changes

Defined in BddFsmCache.c

BddFsmCache_ptr 
BddFsmCache_soft_copy(
  const BddFsmCache_ptr  self 
)
Returns the same instance, but the family counter is increased, in order to handle sharing of the instance. The destructor will actually destroy this instance only when the last family member will be destroyed

See Also BddFsmCache_hard_copy
Defined in BddFsmCache.c

void 
BddFsm_apply_synchronous_product(
  BddFsm_ptr  self, 
  const BddFsm_ptr  other 
)
The result goes into self, no changes on other. Both the two FSMs must be based on the same dd manager. The cache will change, since a new separated family will be created for the internal cache, and it will not be shared anymore with previous family. From the old cache will be reused as much as possible

Side Effects self will change

See Also BddFsmCache_reset_not_reusable_fields_after_product
Defined in BddFsm.c

void 
BddFsm_check_machine(
  const BddFsm_ptr  self 
)
Check that the transition relation is total. If not the case than a deadlock state is printed out. May trigger the computation of reachable states and states without successors.

Defined in BddFsm.c

void 
BddFsm_copy_cache(
  BddFsm_ptr  self, 
  const BddFsm_ptr  other, 
  boolean  keep_family 
)
Copies cached information (reachable states, levels, fair states, etc.) possibly previoulsy calculated by 'other' into self. Call this method when self is qualitatively identical to 'other', but for some reason the trans is organized differently. Call to reuse still valid information calculated by 'other' into self. If keep_family is true, the cache will be reused and not copied, meaning that self will belong to the same family as 'other'. In this case a change in 'other' will have effects also on self (and viceversa). Notice that previoulsy calculated information into 'self' will be lost after the copy.

Defined in BddFsm.c

void 
BddFsm_copy_reachable_states(
  BddFsm_ptr  self, 
  BddFsm_ptr  other, 
  boolean  keep_family, 
  boolean  force_calculation 
)
This method can be called when reachable states among FSMs can be reused, for example when other's reachable states are an over-extimation of self's. Parameter force_calculation forces the calculation of the reachable states of 'other' if needed (i.e. not previoulsy calculated). The two FSMs are allowed to belong to the same family. If parameter keep_family is true, than the original FSM's family will not change, and all the family's members (all the FSMs that have a common relative) will have their reachable states changed accordingly. Otherwise, self will be detached by its own original family (originating a new one), and all relatives will be not changed.

Side Effects Internal cache could change of both self and other

Defined in BddFsm.c

BddFsm_ptr 
BddFsm_copy(
  const BddFsm_ptr  self 
)
Copy constructor for BddFsm

Defined in BddFsm.c

BddFsm_ptr 
BddFsm_create(
  BddEnc_ptr  encoding, 
  BddStates  init, 
  BddInvarStates  invar_states, 
  BddInvarInputs  invar_inputs, 
  BddTrans_ptr  trans, 
  JusticeList_ptr  justice, 
  CompassionList_ptr  compassion 
)
All given bdd are referenced. self becomes the owner of given trans, justice and compassion objects, whereas the encoding is owned by the caller

Defined in BddFsm.c

void 
BddFsm_destroy(
  BddFsm_ptr  self 
)
Destructor of class BddFsm

Defined in BddFsm.c

BddStates 
BddFsm_get_backward_image(
  const BddFsm_ptr  self, 
  BddStates  states 
)
This method computes the backward image of a set S of states, i.e. the set of INVAR states from which some of the INVAR states in S is reachable by means of one single machine transition among those consistent with both the input constraints and the state/input constraints. The backward image of S(X) is computed as follows. a. S1(X) := S(X) and Invar(X) b. S2(X') := S1(X)[x'/x

Defined in BddFsm.c

BddEnc_ptr 
BddFsm_get_bdd_encoding(
  const BddFsm_ptr  self 
)
Returns the be encoding associated with the given fsm instance

Defined in BddFsm.c

CompassionList_ptr 
BddFsm_get_compassion(
  const BddFsm_ptr  self 
)
self keeps the ownership of the returned object

Defined in BddFsm.c

BddStates 
BddFsm_get_constrained_backward_image(
  const BddFsm_ptr  self, 
  BddStates  states, 
  BddStatesInputs  constraints 
)
This method computes the backward image of a set of states S, given a set C(X,I) of contraints on STATE and INPUT vars which are meant to represent a restriction on allowed transitions and inputs. The constrained image is the set of INVAR states from which some of the INVAR states in S is reachable by means of one single machine transition among those consistent with both the machine constraints and the given additional constraint C(X,I). The backward image of S(X,IC) is computed as follows. a. S1(X) := S(X) and Invar(X) b. S2(X') := S1(X)[x'/x

Defined in BddFsm.c

BddStates 
BddFsm_get_constrained_forward_image(
  const BddFsm_ptr  self, 
  BddStates  states, 
  BddStatesInputs  constraints 
)
This method computes the forward image of a set of states S, given a set C(X,I) of contraints on STATE and INPUT vars which are meant to represent a restriction on allowed transitions and inputs. The constrained image is the set of INVAR states which are reachable from one of the INVAR states in S by means of one single machine transition among those consistent with both the constraints defined within the machine and the additional constraint C(X,I). The forward image of S(X,IC) is computed as follows. a. S1(X,I) := S(X) and Invar(X) and InputConst(I) and C(X,I) b. S2(X') := { x' | in Tr(X,I,X') for some in S1(X,I) } c. S3(X) := S2(X')[x/x'

Defined in BddFsm.c

BddStates 
BddFsm_get_deadlock_states(
  BddFsm_ptr  self 
)
This method returns the set of deadlock states. A state ds is said to be a deadlock state when all the following conditions hold: 1) ds is a state satisfying stateConstr; 2) no transition from ds exists which is consistent with input and state/input constraint and leads to a state satisfying stateConstr; 3) s is rechable. Could update the cache. May trigger the computation of reachable states and states without successors. Returned bdd is referenced.

Side Effects Cache can change

Defined in BddFsm.c

int 
BddFsm_get_diameter(
  BddFsm_ptr  self 
)
This method returns an integer which represents the diameter of the machine with respect to the set of initial states, i.e. the distance of the fatherst state in the machine (starting from the initial states), i.e. the maximal value among the lengths of shortest paths to each reachable state. The initial diameter is computed as the number of iteration the fixpoint procedure described above (see "BddFsm_get_reachable_states") does before reaching the fixpoint. It can also be seen as the maximal value the "BddFsm_get_distance_of_states" can return (which is returned when the argument "states" is set to "all the states"). Could update the cache.

Side Effects Internal cache could change

Defined in BddFsm.c

int 
BddFsm_get_distance_of_states(
  BddFsm_ptr  self, 
  BddStates  states 
)
Computes the set of reachable states if not previously cached. Returns -1 if given states set is not reachable. This method returns an integer which represents the distance of the farthest state in "states". The distance of one single state "s" is the number of applications of the "BddFsm_get_forward_image" method (starting from the initial set of states) which is necessary and sufficient to end up with a set of states containing "s". The distance of a *set* of states "set" is the maximal distance of states in "set", i.e. the number of applications of the "BddFsm_get_forward_image" method (starting from the initial set of states) which is necessary and sufficient to reach at least once (not necessarily during the last application, but somewhere along the way) each state in "set". So, the distance of a set of states is a max-min function. Could update the cache.

Side Effects Internal cache could change

Defined in BddFsm.c

BddStatesInputs 
BddFsm_get_fair_states_inputs(
  BddFsm_ptr  self 
)
Returns the set of fair state-input pairs of the machine.

Side Effects Internal cache could change

Defined in BddFsm.c

BddStates 
BddFsm_get_fair_states(
  BddFsm_ptr  self 
)
Returns the set of fair states of a fsm.

Side Effects Internal cache could change

Defined in BddFsm.c

BddStates 
BddFsm_get_forward_image(
  const BddFsm_ptr  self, 
  BddStates  states 
)
This method computes the forward image of a set of states S, i.e. the set of INVAR states which are reachable from one of the INVAR states in S by means of one single machine transition among those consistent with both the input constraints and the state/input constraints. The forward image of S(X) is computed as follows. a. S1(X,I) := S(X) and Invar(X) and InputConst(I) b. S2(X') := { x' | in Tr(X,I,X') for some in S1(X,I) } c. S3(X) := S2(X')[x/x'

Defined in BddFsm.c

BddStates 
BddFsm_get_init(
  const BddFsm_ptr  self 
)
Returned bdd is referenced

Defined in BddFsm.c

BddInvarInputs 
BddFsm_get_input_constraints(
  const BddFsm_ptr  self 
)
Returned bdd is referenced

Defined in BddFsm.c

JusticeList_ptr 
BddFsm_get_justice(
  const BddFsm_ptr  self 
)
self keeps the ownership of the returned object

Defined in BddFsm.c

BddStatesInputs 
BddFsm_get_k_backward_image(
  const BddFsm_ptr  self, 
  BddStates  states, 
  int  k 
)
This method computes the set of couples that lead into at least k distinct states of the set of states given as input. The returned couples and the states in the set given in input are restricted The k-backward image of S(X) is computed as follows. a. S1(X) := S(X) and Invar(X) b. S2(X') := S1(X)[X'/X

Defined in BddFsm.c

bdd_ptr 
BddFsm_get_monolithic_trans_bdd(
  BddFsm_ptr  self 
)
This method returns a monolithic representation of the transition relation, which is computed on the basis of the internal partitioned representation by composing all the element of the partition. Returned bdd is referenced.

Side Effects Internal cache could change

Defined in BddFsm.c

BddStates 
BddFsm_get_not_successor_states(
  BddFsm_ptr  self 
)
This method returns the set of states with no successor. A state "ds" has no successor when all the following conditions hold: 1) ds is a state satisfying stateConstr. 2) no transition from ds exists which is consistent with input and state/input constraint and leads to a state satisfying stateConstr. Could update the cache.

Side Effects Internal cache could change

Defined in BddFsm.c

BddStates 
BddFsm_get_reachable_states_at_distance(
  BddFsm_ptr  self, 
  int  distance 
)
Computes the set of reachable states if not previously, cached. Returned bdd is referenced. If distance is greater than the diameter, an assertion is fired. This method returns the set R of states of this machine which can be reached in exactly "distance" steps by applying the "BddFsm_get_forward_image" method ("distance" times) starting from one of the initial states (and cannot be reached with less than "distance" steps). In the case that the distance is less than 0, the empty-set is returned. These states are computed as intermediate steps of the fixpoint characterization given in the "BddFsm_get_reachable_states" method.

Side Effects Internal cache could change

Defined in BddFsm.c

BddStates 
BddFsm_get_reachable_states(
  BddFsm_ptr  self 
)
Returned bdd is referenced. This method returns the set R of reachable states, i.e. those states that can be actually reached starting from one of the initial state. R is the set of states such that "i TRC s" holds for some state i in the set of initial states, where TRC is the transitive closure of the conjunction of the transition relation of the machine with the set of invar states, the set of constraints on inputs and the set of state/input constraints. R is computed by this method in a forward manner by exploiting the "BddFsm_get_forward_image" method during a fixpoint calculation. In particular, R is computed by reaching the fixpoint on the functional that maps S onto the forward image BddFsm_get_forward_image(S) of S, where the computation is started from the set of initial states. Notice that the set of invar states, the set of constraints on inputs and the set of state/input constrains are implicitly taken into account by BddFsm_get_forward_image(S).

Side Effects Internal cache could change

Defined in BddFsm.c

BddInvarStates 
BddFsm_get_state_constraints(
  const BddFsm_ptr  self 
)
Returned bdd is referenced

Defined in BddFsm.c

BddStatesInputs 
BddFsm_get_states_inputs_constraints(
  const BddFsm_ptr  self 
)
Returns a state-input pair for which at least one legal successor exists

Defined in BddFsm.c

BddStatesInputs 
BddFsm_get_strong_backward_image(
  const BddFsm_ptr  self, 
  BddStates  states 
)
This method computes the set of transitions that have at least one successor and are such that all the successors lay inside the INVAR subset of the set of states given as input. The strong backward image of S(X, I) is computed as follows. a. S1(X,I) := WeakBwdImg(not S(X)) b. S2(X,I) := (not S1(X,I)) and StateConstr(X) and InputConst(I) c. Tr(X,I) := { | in Tr(X,I,X') for some x'} d. StrongBwdImg(X,I) := S2(X,I) and Tr(X,I) Returned bdd is referenced.

Defined in BddFsm.c

BddTrans_ptr 
BddFsm_get_trans(
  const BddFsm_ptr  self 
)
Returned Trans instance is not copied, do not destroy it, since self keeps the ownership.

Defined in BddFsm.c

BddStatesInputs 
BddFsm_get_weak_backward_image(
  const BddFsm_ptr  self, 
  BddStates  states 
)
This method computes the set of couples that leads into the set of states given as input. i.e. the set of couples such that is consistent with both the input constraints and the state/input constraints, s is INVAR, and a transition from s to s' labelled by i exists for some INVAR s' in S. The weak backward image of S(X) is computed as follows. a. S1(X) := S(X) and Invar(X) b. S2(X') := S1(X)[x'/x

Defined in BddFsm.c

boolean 
BddFsm_is_deadlock_free(
  BddFsm_ptr  self 
)
This method checks wether this machine is deadlock free, i.e. wether it is impossible to reach an INVAR state with no admittable INVAR successor moving from the initial condition. This happens when the machine is total. If it is not, each INVAR state from which no transition to another INVAR state can be made according to the input and state/input constraints is non-reachable. This method checks deadlock freeness by checking that the intersection between the set of reachable states and the set of INVAR states with no admittable INVAR successor is empty. Could update the cache. May trigger the computation of deadlock states.

Side Effects Cache can change

Defined in BddFsm.c

boolean 
BddFsm_is_fair_states(
  const BddFsm_ptr  self, 
  BddStates  states 
)
Checks if a set of states is fair.

Defined in BddFsm.c

boolean 
BddFsm_is_total(
  BddFsm_ptr  self 
)
This method checks wether this machine is total, in the sense that each INVAR state has at least one INVAR successor state given the constraints on the inputs and the state/input. This is done by checking that the BddFsm_ImageBwd image of the set of all the states is the set of all the INVAR states. This way, the INVAR constraints together with the set of constraints on both input and state/input are implicitly taken into account by BddFsm_get_forward_image. The answer "false" is produced when states exist that admit no INVAR successor, given the sets of input and state/input constraints. However, all these "dead" states may be non-reachable, so the machine can still be "deadlock free". See the "BddFsm_is_deadlock_free" method. Could update the cache. May trigger the computation of states without successors.

Side Effects Cache can change

Defined in BddFsm.c

void 
BddFsm_print_fair_states_info(
  const BddFsm_ptr  self, 
  const boolean  print_states, 
  FILE* file 
)
Prints the number of fair states, taking care of the encoding and of the indifferent variables in the encoding. In verbose mode also prints states.

Defined in BddFsm.c

void 
BddFsm_print_fair_transitions_info(
  const BddFsm_ptr  self, 
  const boolean  print_transitions, 
  FILE* file 
)
Prints the number of fair states, taking care of the encoding and of the indifferent variables in the encoding.

Defined in BddFsm.c

void 
BddFsm_print_info(
  const BddFsm_ptr  self, 
  FILE* file 
)
Prints some information about this BddFsm.

Side Effects None

Defined in BddFsm.c

void 
BddFsm_print_reachable_states_info(
  const BddFsm_ptr  self, 
  const boolean  print_states, 
  FILE* file 
)
Prints statistical information about reachable states, i.e. the real number of reachable states. It is computed taking care of the encoding and of the indifferent variables in the encoding.

Defined in BddFsm.c

boolean 
BddFsm_reachable_states_computed(
  BddFsm_ptr  self 
)
Returns true if the set of reachable states has already been computed

Defined in BddFsm.c

BddStates 
BddFsm_states_inputs_to_inputs(
  const BddFsm_ptr  self, 
  BddStatesInputs  si 
)
Quantifies away the state variables.

Defined in BddFsm.c

BddStates 
BddFsm_states_inputs_to_states(
  const BddFsm_ptr  self, 
  BddStatesInputs  si 
)
Quantifies away the input variables.

Defined in BddFsm.c

BddInputs 
BddFsm_states_to_states_get_inputs(
  const BddFsm_ptr  self, 
  BddStates  cur_states, 
  BddStates  next_states 
)
Given two sets of states, returns the set of inputs labeling any transition from a state in the first set to a state in the second set.

Defined in BddFsm.c

void 
Bdd_End(
    
)
Quit the BddFsm package

Defined in bddCmd.c

void 
Bdd_Init(
    
)
Initializes the BddFsm package.

Defined in bddCmd.c

int 
CommandCheckFsm(
  int  argc, 
  char ** argv 
)
Checks the fsm for totality and deadlock states.

Defined in bddCmd.c

int 
CommandComputeReachable(
  int  argc, 
  char ** argv 
)
Enables the future computation of the set of reachable states

Defined in bddCmd.c

int 
CommandPrintFairStates(
  int  argc, 
  char ** argv 
)
Prints the fair states.

Defined in bddCmd.c

int 
CommandPrintFairTransitions(
  int  argc, 
  char ** argv 
)
Prints the fair transitions.

Defined in bddCmd.c

int 
CommandPrintReachableStates(
  int  argc, 
  char ** argv 
)
Prints the reachable states.

Defined in bddCmd.c

void 
CompassionList_append_p_q(
  CompassionList_ptr  self, 
  BddStates  p, 
  BddStates  q 
)
Given bdds are referenced, so the caller should free it when it is no longer needed

Defined in FairnessList.c

void 
CompassionList_apply_synchronous_product(
  CompassionList_ptr  self, 
  const CompassionList_ptr  other 
)
Creates the union of the two given fairness lists. Result goes into self

Side Effects self changes

Defined in FairnessList.c

CompassionList_ptr 
CompassionList_create(
  DdManager* dd_manager 
)
Call FairnessList_destroy to destruct self

Defined in FairnessList.c

BddStates 
CompassionList_get_p(
  const CompassionList_ptr  self, 
  const FairnessListIterator_ptr  iter 
)
Returned bdd is referenced

Defined in FairnessList.c

BddStates 
CompassionList_get_q(
  const CompassionList_ptr  self, 
  const FairnessListIterator_ptr  iter 
)
Returned bdd is referenced

Defined in FairnessList.c

boolean 
FairnessListIterator_is_end(
  const FairnessListIterator_ptr  self 
)
Use to check end of iteration

Defined in FairnessList.c

FairnessListIterator_ptr 
FairnessListIterator_next(
  const FairnessListIterator_ptr  self 
)
use to iterate on an list iterator

Defined in FairnessList.c

FairnessListIterator_ptr 
FairnessList_begin(
  const FairnessList_ptr  self 
)
Use to start iteration

Defined in FairnessList.c

FairnessList_ptr 
FairnessList_create(
  DdManager* dd_manager 
)
Base class constructor

Defined in FairnessList.c

void 
JusticeList_append_p(
  JusticeList_ptr  self, 
  BddStates  p 
)
Given bdd is referenced, so the caller should free it when it is no longer needed

Defined in FairnessList.c

void 
JusticeList_apply_synchronous_product(
  JusticeList_ptr  self, 
  const JusticeList_ptr  other 
)
Creates the union of the two given fairness lists. Result goes into self

Side Effects self changes

Defined in FairnessList.c

JusticeList_ptr 
JusticeList_create(
  DdManager* dd_manager 
)
Call FairnessList_destroy to destruct self

Defined in FairnessList.c

BddStates 
JusticeList_get_p(
  const JusticeList_ptr  self, 
  const FairnessListIterator_ptr  iter 
)
Returned bdd is referenced

Defined in FairnessList.c

static BddStatesInputs 
bdd_fsm_EU_SI(
  const BddFsm_ptr  self, 
  BddStatesInputs  f, 
  BddStatesInputs  g 
)
Computes the set of state-input pairs that satisfy E(f U g), with f and g sets of state-input pairs.

Defined in BddFsm.c

static BddStatesInputs 
bdd_fsm_EX_SI(
  const BddFsm_ptr  self, 
  BddStatesInputs  si 
)
Quantifies away the inputs, and computes the (states-inputs) preimage of the resulting set of states.

Defined in BddFsm.c

static void 
bdd_fsm_cache_deinit_reachables(
  BddFsmCache_ptr  self 
)
Call only if family_counter is 0

Defined in BddFsmCache.c

static void 
bdd_fsm_cache_deinit(
  BddFsmCache_ptr  self 
)
private deinitializer. Call only if family_counter is 0

Defined in BddFsmCache.c

static void 
bdd_fsm_cache_init(
  BddFsmCache_ptr  self, 
  DdManager* dd 
)
private initializer

Defined in BddFsmCache.c

static void 
bdd_fsm_check_fairness_emptiness(
  const BddFsm_ptr  self 
)
Checks fair states for emptiness, as well as fot the intersaction of fair states and inits. Prints a warning if needed

Defined in BddFsm.c

static void 
bdd_fsm_check_init_state_invar_emptiness(
  const BddFsm_ptr  self 
)
Check inits for emptiness, and prints a warning if needed

Defined in BddFsm.c

static void 
bdd_fsm_compute_reachable_states(
  BddFsm_ptr  self 
)
Returned bdd is referenced

Side Effects Changes the internal cache

Defined in BddFsm.c

static void 
bdd_fsm_copy(
  const BddFsm_ptr  self, 
  BddFsm_ptr  copy 
)
private copy constructor

Defined in BddFsm.c

static void 
bdd_fsm_deinit(
  BddFsm_ptr  self 
)
private member called by the destructor

Defined in BddFsm.c

static BddStatesInputs 
bdd_fsm_fair_SI_subset_aux(
  const BddFsm_ptr  self, 
  BddStatesInputs  states, 
  BddStatesInputs  subspace 
)

Defined in BddFsm.c

static BddStatesInputs 
bdd_fsm_get_fair_SI_subset(
  const BddFsm_ptr  self, 
  BddStatesInputs  subspace 
)

Defined in BddFsm.c

static BddStatesInputs 
bdd_fsm_get_fair_states_inputs_in_subspace(
  const BddFsm_ptr  self, 
  BddStatesInputs  subspace 
)

Defined in BddFsm.c

static BddStatesInputs 
bdd_fsm_get_legal_state_input(
  BddFsm_ptr  self 
)
A legal transition is a transition which satisfy the transition relation, and the state, input and next-state satisfy the invariants. So the image S(X, I) is computed as follows: S(X,I) = StateConstr(X) & InputConstr(i) & StateConstr(X') & Tr(X,I,X') for some X' Used for planning in strong backward image computation. Could update the cache. Returned bdd is referenced.

Side Effects Cache can change

Defined in BddFsm.c

static void 
bdd_fsm_init(
  BddFsm_ptr  self, 
  BddEnc_ptr  encoding, 
  BddStates  init, 
  BddInvarStates  invar_states, 
  BddInvarInputs  invar_inputs, 
  BddTrans_ptr  trans, 
  JusticeList_ptr  justice, 
  CompassionList_ptr  compassion 
)
Private initializer

Defined in BddFsm.c

static void 
fairness_list_init(
  FairnessList_ptr  self, 
  DdManager* dd_manager 
)

Defined in FairnessList.c

Last updated on 2009/01/30 15h:04