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_reachable_states(
  BddFsmCache_ptr  self, 
  BddStates  reachable 
)
Fills cache structure with reachable states information. The given BDD is supposed to represent the whole set of reachable states of the Bdd FSM. It should NOT contain other informations (such as onion rings ecc)

Defined in BddFsmCache.c 

void 
BddFsmCache_set_reachables(
  BddFsmCache_ptr  self, 
  node_ptr  layers_list, 
  const int  diameter, 
  boolean  completed 
)
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_custom_varsets(
  BddFsm_ptr  self, 
  const BddFsm_ptr  other, 
  bdd_ptr  state_vars_cube, 
  bdd_ptr  input_vars_cube, 
  bdd_ptr  next_vars_cube 
)
Original description for BddFsm_apply_synchronous_product: 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. Modified part: Takes cubes of state, input, and next state variables as arguments (rather than obtaining the cubes of all these variables from the bdd encoding). This is supposed to avoid problems when only subsets of variables need to be considered (as is the case for games).

Side Effects self will change

See Also BddFsm_apply_synchronous_product BddFsmCache_reset_not_reusable_fields_after_product
Defined in BddFsm.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 BddFsm_apply_synchronous_product_custom_varsets 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 

boolean 
BddFsm_expand_cached_reachable_states(
  BddFsm_ptr  self, 
  int  k, 
  int  max_seconds 
)
If k<0 the set is expanded until fixpoint, if max_seconds<0 no time limit is considered

Side Effects Changes the internal cache

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,F) is computed as follows. X - state variables, I - input variables, F - frozen variables. a. S1(X,F) := S(X,F) and Invar(X,F) b. S2(X',F) := S1(X,F)[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 

boolean 
BddFsm_get_cached_reachable_states(
  const BddFsm_ptr  self, 
  BddStates** layers, 
  int* size 
)
Returns the cached reachable states

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, 
  BddStatesInputsNexts  constraints 
)
This method computes the backward image of a set of states S, given a set C(X,F,I) of contraints on STATE, FROZEN 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,F,I). The backward image of S(X,F,I) is computed as follows. X - state variables, I - input variables, F - frozen variables. a. S1(X,F) := S(X,F) and Invar(X,F) b. S2(X',F) := S1(X,F)[x'/x

Defined in BddFsm.c 

BddStatesInputs 
BddFsm_get_constrained_forward_image_states_inputs(
  const BddFsm_ptr  self, 
  BddStatesInputs  si, 
  BddStatesInputsNexts  constraints 
)
This method computes the forward image of a set of state-input pairs SI constrained by constraints (from now on C). This is the set of state-input pairs that fulfills INVAR and INPUT constraints and can be reached via a legal transition from at least one member of SI that itself must fulfill INVAR, INPUT, and C. The forward image of SI(X,F,I) is computed as follows. X - state variables, F - frozen variables, I - input variables. a. S1(X,F,I) := SI(X,F,I) and Invar(X,F) and Input(I) and C(X,F,I) b. S2(X',F) := { | in Tr(X,F,I,X') for some in S1(X,F,I) } c. S3(X,F) := S2(X',F)[x/x'

See Also BddFsm_get_forward_image_states_inputs BddFsm_get_constrained_forward_image
Defined in BddFsm.c 

BddStates 
BddFsm_get_constrained_forward_image(
  const BddFsm_ptr  self, 
  BddStates  states, 
  BddStatesInputsNexts  constraints 
)
This method computes the forward image of a set of states S, given a set C of contraints on STATE, FROZEN 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,F,I). The forward image of S(X,F) is computed as follows. X - state variables, I - input variables, F - frozen variables. a. S1(X,F,I) := S(X,F) and Invar(X,F) and InputConst(I) and C(X,F,I) b. S2(X',F) := { | in Tr(X,F,I,X') for some in S1(X,F,I) } c. S3(X,F) := S2(X',F)[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. Note: a state is represented by state and frozen variables.

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 
)
A state-input pair is fair iff it can reach a cycle that visits all fairness constraints. Note: a state is represented by state and frozen variables.

Side Effects Internal cache could change

Defined in BddFsm.c 

BddStates 
BddFsm_get_fair_states(
  BddFsm_ptr  self 
)
A state is fair iff it can reach a cycle that visits all fairness constraints. Note: a state is represented by state and frozen variables.

Side Effects Internal cache could change

Defined in BddFsm.c 

BddStatesInputs 
BddFsm_get_forward_image_states_inputs(
  const BddFsm_ptr  self, 
  BddStatesInputs  si 
)
This method computes the forward image of a set of state-input pairs SI. This is the set of state-input pairs that fulfills INVAR and INPUT constraints and can be reached via a legal transition from at least one member of si that itself must fulfill INVAR and INPUT. The forward image of SI(X,F,I) is computed as follows. X - state variables, F - frozen variables, I - input variables. a. S1(X,F,I) := SI(X,F,I) and Invar(X,F) and Input(I) b. S2(X',F) := { | in Tr(X,F,I,X') for some in S1(X,F,I) } c. S3(X,F) := S2(X',F)[x/x'

See Also BddFsm_get_constrained_forward_image_states_inputs BddFsm_get_forward_image
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,F) is computed as follows. X - state variables, I - input variables, F - frozen variables. a. S1(X,F,I) := S(X,F) and Invar(X,F) and InputConst(I) b. S2(X',F) := { | in Tr(X,F,I,X') for some in S1(X,F,I) } c. S3(X,F) := S2(X',F)[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 tuples 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,F) is computed as follows. X - state variables, I - input variables, F - frozen variables. a. S1(X,F) := S(X,F) and Invar(X,F) b. S2(X',F) := S1(X,F)[X'/X

Defined in BddFsm.c 

int 
BddFsm_get_minimum_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 nearest 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". Could update the cache.

Side Effects Internal cache could change

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. Note: a state is represented by state and frozen variables.

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. Note: a state is represented by state and frozen variables.

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). Note: a state is represented by state and frozen variables.

Side Effects Internal cache could change

Defined in BddFsm.c 

BddStatesInputs 
BddFsm_get_revfair_states_inputs(
  BddFsm_ptr  self 
)
A state-input pair is reverse fair iff it can be reached from a cycle that visits all fairness constraints. Note: a state is represented by state and frozen variables.

Side Effects Internal cache could change

Defined in BddFsm.c 

BddStates 
BddFsm_get_revfair_states(
  BddFsm_ptr  self 
)
A state is reverse fair iff it can be reached from a cycle that visits all fairness constraints. Note: a state is represented by state and frozen variables.

Side Effects Internal cache could change

Defined in BddFsm.c 

BddStates 
BddFsm_get_sins_constrained_forward_image(
  const BddFsm_ptr  self, 
  BddStates  states, 
  BddStatesInputsNexts  constraints 
)
This method computes the forward image of a set of states S, given a set C of contraints on STATE, FROZEN and INPUT and NEXT 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,F,I). The forward image of S(X,F) is computed as follows. X - state variables, I - input variables, F - frozen variables. a. S1(X,F,I) := S(X,F) and Invar(X,F) and InputConst(I) and C(X,F,I) b. S2(X',F) := { | in Tr(X,F,I,X') for some in S1(X,F,I) } c. S3(X,F) := S2(X',F)[x/x'

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, 
  BddFsm_dir  dir 
)
Returns a state-input pair for which at least one legal successor (if dir = BDD_FSM_DIR_BWD) or predecessor (otherwise) 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, F, I) is computed as follows. X - state variables, I - input variables, F - frozen variables. a. S1(X,F,I) := WeakBwdImg(not S(X,F)) b. S2(X,F,I) := (not S1(X,F,I)) and StateConstr(X,F) and InputConst(I) c. Tr(X,F,I) := { | in Tr(X,F,I,X') for some x'} d. StrongBwdImg(X,F,I) := S2(X,F,I) and Tr(X,F,I) Note: a state is represented by state and frozen variables, but frozen variable are never abstracted away. 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 tuples that leads into the set of states given as input. i.e. the set of 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,F) is computed as follows. X - state variables, I - input variables, F - frozen variables. a. S1(X,F) := S(X,F) and Invar(X,F) b. S2(X',F := S1(X,F)[x'/x

Defined in BddFsm.c 

boolean 
BddFsm_has_cached_reachable_states(
  const BddFsm_ptr  self 
)
Checks if the set of reachable states exists in the FSM

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, 
  const boolean  print_defines, 
  const boolean  print_formula, 
  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 
)
Note: a state is represented by state and frozen variables.

Defined in BddFsm.c 

void 
BddFsm_set_reachable_states(
  const BddFsm_ptr  self, 
  BddStates  reachable 
)
Sets the whole set of reachable states for this FSM, with no onion ring informations

Defined in BddFsm.c 

BddStates 
BddFsm_states_inputs_to_inputs(
  const BddFsm_ptr  self, 
  BddStatesInputs  si 
)
Quantifies away the state variables (including frozen ones). A state is represented by state and frozen variables thus both state and frozen variables are abstracted away.

Defined in BddFsm.c 

BddStates 
BddFsm_states_inputs_to_states(
  const BddFsm_ptr  self, 
  BddStatesInputs  si 
)
Quantifies away the input variables. Note: a state is represented by state and frozen variables.

Defined in BddFsm.c 

BddInputs 
BddFsm_states_to_states_get_inputs(
  const BddFsm_ptr  self, 
  BddStates  cur_states, 
  BddStates  next_states 
)
Note: a state is represented by state and frozen variables.

Defined in BddFsm.c 

void 
BddFsm_update_cached_reachable_states(
  const BddFsm_ptr  self, 
  node_ptr  layers_list, 
  int  size, 
  boolean  completed 
)
Updates the cached reachable states

Defined in BddFsm.c 

BddOregJusticeEmptinessBddAlgorithmType \ 
Bdd_BddOregJusticeEmptinessBddAlgorithmType_from_string(
  const char* name 
)
Converts the given type from string "name" to a BddOregJusticeEmptinessBddAlgorithmType object.

Side Effects None.

See Also BddOregJusticeEmptinessBddAlgorithmType_to_string
Defined in bddMisc.c 

const char* 
Bdd_BddOregJusticeEmptinessBddAlgorithmType_to_string(
  const BddOregJusticeEmptinessBddAlgorithmType  self 
)
It takes BddOregJusticeEmptinessBddAlgorithmType of self and returns a string specifying the type of it. Returned string is statically allocated and must not be freed.

Side Effects None.

See Also Bdd_BddOregJusticeEmptinessBddAlgorithmType_from_string
Defined in bddMisc.c 

void 
Bdd_End(
    
)
Quit the BddFsm package

Defined in bddCmd.c 

void 
Bdd_Init(
    
)
Initializes the BddFsm package.

Defined in bddCmd.c 

boolean 
Bdd_elfwd_check_options(
  unsigned int  which_options, 
  boolean  on_fail_print 
)
Depending on the value of which_options, it checks that forward search, ltl_tableau_forward_search, and use_reachable_states are enabled and counter_examples is disabled. Returns true if the checks are successful, false otherwise. If on_fail_print is true, it prints an error message on failure.

Side Effects None.

Defined in bddMisc.c 

BddELFwdSavedOptions_ptr 
Bdd_elfwd_check_set_and_save_options(
  unsigned int  which_options 
)
Which values are actually checked, set, and saved is determined by the value of which_options. If set in which_options, forward search, ltl_tableau_forward_search, and use_reachable_states are enabled and counter_examples is disabled. Previous values are stored and returned. Creates the returned BddELFwdSavedOptions_ptr. It does *not* belong to caller - it will be destroyed by the corresponding call to Bdd_elfwd_restore_options.

Side Effects Modifies options.

See Also Bdd_elfwd_restore_options
Defined in bddMisc.c 

void 
Bdd_elfwd_restore_options(
  unsigned int  which_options, 
  BddELFwdSavedOptions_ptr  saved_options 
)
Which values are actually restored from saved_options is determined by the value of which_options.

Side Effects Modifies options.

See Also Bdd_elfwd_check_set_and_save_options
Defined in bddMisc.c 

void 
Bdd_print_available_BddOregJusticeEmptinessBddAlgorithms(
  FILE * file 
)
Prints the BDD-based algorithms to check language emptiness for omega-regular properties the system currently supplies

Side Effects None.

See Also BddOregJusticeEmptinessBddAlgorithmType Bdd_BddOregJusticeEmptinessBddAlgorithmType_to_string
Defined in bddMisc.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 
)
Computates 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_EUorES_SI(
  const BddFsm_ptr  self, 
  BddStatesInputs  f, 
  BddStatesInputs  g, 
  BddFsm_dir  dir 
)
Computes the set of state-input pairs that satisfy E(f U g) (if dir = BDD_FSM_DIR_BWD) or E(f S g) (otherwise), with f and g sets of state-input pairs.

Defined in BddFsm.c 

static BddStatesInputs 
bdd_fsm_EXorEY_SI(
  const BddFsm_ptr  self, 
  BddStatesInputs  si, 
  BddFsm_dir  dir 
)
Preimage: Quantifies away the inputs, and computes the (states-inputs) preimage of the resulting set of states. Postimage: Computes the (states-inputs) postimage of si.

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 BddStatesInputs 
bdd_fsm_compute_EL_SI_subset_aux(
  const BddFsm_ptr  self, 
  BddStatesInputs  states, 
  BddStatesInputs  subspace, 
  BddFsm_dir  dir 
)
Executes the inner fixed point of the Emerson-Lei algorithm. Direction is given by dir, fair states are restricted to states, backward/forward exploration (other than the last, "strict" image) is restricted to subspace.

Defined in BddFsm.c 

static BddStatesInputs 
bdd_fsm_compute_EL_SI_subset(
  const BddFsm_ptr  self, 
  BddStatesInputs  subspace, 
  BddFsm_dir  dir 
)
Executes the Emerson-Lei algorithm in the set of states given by subspace in the direction given by dir

Defined in BddFsm.c 

static void 
bdd_fsm_compute_reachable_states(
  BddFsm_ptr  self 
)
Computes the set of reachable states of this machine

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_get_fair_or_revfair_states_inputs_in_subspace(
  const BddFsm_ptr  self, 
  BddStatesInputs  subspace, 
  BddFsm_dir  dir 
)
Computes the set of fair states (if dir = BDD_FSM_DIR_BWD) or reverse fair states (otherwise) by calling the Emerson-Lei algorithm.

Defined in BddFsm.c 

static BddStatesInputs 
bdd_fsm_get_fair_or_revfair_states_inputs(
  BddFsm_ptr  self, 
  BddFsm_dir  dir 
)
Computes the set of fair states (if dir = BDD_FSM_DIR_BWD) or reverse fair states (otherwise) by calling the Emerson-Lei algorithm.

Side Effects Cache might change

See Also bdd_fsm_get_fair_or_revfair_states_inputs_in_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, F, I) is computed as follows: S(X,F,I) = StateConstr(X,F) & InputConstr(i) & StateConstr(X',F) & Tr(X,F,I,X') for some X' X - state variables, I - input variables, F - frozen variables. Used for planning in strong backward image computation. Could update the cache. Note: a state is represented by state and frozen variables, but frozen variable are never abstracted away. 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 2011/04/06 21h:12