|
spot
2.16
|
A loaded LTSmin model that can generate Kripke structures on-the-fly. More...
#include <spot/ltsmin/ltsmin.hh>
Public Member Functions | |
| kripke_ptr | kripke (const atomic_prop_set *to_observe, bdd_dict_ptr dict, formula dead=formula::tt(), int compress=0) const |
| Generate a Kripke structure on-the-fly. More... | |
| ltsmin_kripkecube_ptr | kripkecube (std::vector< std::string > to_observe, formula dead=formula::tt(), int compress=0, unsigned int nb_threads=1) const |
| The same as above but returns a kripkecube, i.e., a kripke that can be used in parallel. Moreover, it supports more elaborate atomic propositions such as "P.a == P.c". More... | |
| int | state_size () const |
| Number of variables in a state. More... | |
| const char * | state_variable_name (int var) const |
| Name of each variable. More... | |
| int | state_variable_type (int var) const |
| Type of each variable. More... | |
| int | type_count () const |
| Number of different types. More... | |
| const char * | type_name (int type) const |
| Name of each type. More... | |
| int | type_value_count (int type) |
| Count of enumerated values for a type. More... | |
| const char * | type_value_name (int type, int val) |
| Name of each enumerated value for a type. More... | |
Static Public Member Functions | |
| static ltsmin_model | load (const std::string &file) |
| Load an ltsmin model, either from divine or promela. More... | |
A loaded LTSmin model that can generate Kripke structures on-the-fly.
| kripke_ptr spot::ltsmin_model::kripke | ( | const atomic_prop_set * | to_observe, |
| bdd_dict_ptr | dict, | ||
| formula | dead = formula::tt(), |
||
| int | compress = 0 |
||
| ) | const |
Generate a Kripke structure on-the-fly.
The dead parameter is used to control the behavior of the model on dead states (i.e. the final states of finite sequences). If DEAD is formula::ff(), it means we are not interested in finite sequences of the system, and dead state will have no successor. If DEAD is formula::tt(), we want to check finite sequences as well as infinite sequences, but do not need to distinguish them. In that case dead state will have a loop labeled by true. If DEAD is any atomic proposition (formula::ap("...")), this is the name of a property that should be true when looping on a dead state, and false otherwise.
This function returns nullptr on error.
to_observe the list of atomic propositions that should be observed in the model dict the BDD dictionary to use dead an atomic proposition or constant to use for looping on dead states compress whether to compress the states. Use 0 to disable, 1 to enable compression, 2 to enable a faster compression that only works if all variables are smaller than 2^28.
| ltsmin_kripkecube_ptr spot::ltsmin_model::kripkecube | ( | std::vector< std::string > | to_observe, |
| formula | dead = formula::tt(), |
||
| int | compress = 0, |
||
| unsigned int | nb_threads = 1 |
||
| ) | const |
The same as above but returns a kripkecube, i.e., a kripke that can be used in parallel. Moreover, it supports more elaborate atomic propositions such as "P.a == P.c".
|
static |
Load an ltsmin model, either from divine or promela.
The filename given can be either a *.pm/*.pml/*.prom promela source or a *.spins dynamic library compiled with "spins file". If a promela source is supplied, this function will call spins to update the *.spins library only if it is not newer.
Similarly the divine models can be specified as *.dve source or *.dve or *.dve2C libraries.
| int spot::ltsmin_model::state_size | ( | ) | const |
Number of variables in a state.
| const char* spot::ltsmin_model::state_variable_name | ( | int | var | ) | const |
Name of each variable.
| int spot::ltsmin_model::state_variable_type | ( | int | var | ) | const |
Type of each variable.
| int spot::ltsmin_model::type_count | ( | ) | const |
Number of different types.
| const char* spot::ltsmin_model::type_name | ( | int | type | ) | const |
Name of each type.
| int spot::ltsmin_model::type_value_count | ( | int | type | ) |
Count of enumerated values for a type.
| const char* spot::ltsmin_model::type_value_name | ( | int | type, |
| int | val | ||
| ) |
Name of each enumerated value for a type.
1.9.1