spot  2.11.2
Classes | Typedefs | Enumerations | Functions | Variables
spot Namespace Reference

Classes

class  digraph
 A directed graph. More...
 
class  named_graph
 
class  fair_kripke_succ_iterator
 Iterator code for a Fair Kripke structure. More...
 
class  fair_kripke
 Interface for a Fair Kripke structure. More...
 
class  kripkecube
 This class is a template representation of a Kripke structure. It is composed of two template parameters: State represents a state of the Kripke structure, SuccIterator is an iterator over the (possible) successors of a state. More...
 
class  is_a_kripkecube_ptr
 This class allows to ensure (at compile time) if a given parameter is of type kripkecube. It also check if the iterator has the good interface. More...
 
class  kripke_succ_iterator
 Iterator code for Kripke structure. More...
 
class  kripke
 Interface for a Kripke structure. More...
 
struct  kripke_graph_state
 Concrete class for kripke_graph states. More...
 
class  kripke_graph_succ_iterator
 
class  kripke_graph
 Kripke Structure. More...
 
class  ltsmin_model
 
struct  transition_info
 
class  spins_interface
 Implementation of the PINS interface. This class is a wrapper that, given a file, will compile it w.r.t the PINS interface. The class can then be menipulated transparently whatever the input format considered. More...
 
struct  cspins_state_equal
 This class provides the ability to compare two states. More...
 
struct  cspins_state_hash
 This class provides the ability to hash a state. More...
 
class  cspins_state_manager
 The management of states (i.e. allocation/deallocation) can be painless since every time we have to consider wether the state will be compressed or not. This class aims to simplify this management. More...
 
struct  inner_callback_parameters
 
class  cspins_iterator
 This class provides an iterator over the successors of a state. All successors are computed once when an iterator is recycled or created. More...
 
class  kripkecube< cspins_state, cspins_iterator >
 
class  iterable_uf
 
class  swarmed_bloemen
 This class implements the SCC decomposition algorithm of bloemen as described in PPOPP'16. It uses a shared union-find augmented to manage work stealing between threads. More...
 
class  iterable_uf_ec
 
class  swarmed_bloemen_ec
 This class implements the SCC decomposition algorithm of bloemen as described in PPOPP'16. It uses a shared union-find augmented to manage work stealing between threads. More...
 
class  swarmed_cndfs
 
class  swarmed_deadlock
 This class aims to explore a model to detect wether it contains a deadlock. This deadlock detection performs a DFS traversal sharing information shared among multiple threads. If Deadlock equals std::true_type performs dealock algorithm, otherwise perform a simple reachability. More...
 
class  lpar13
 This class implements the sequential emptiness check as presented in "Three SCC-based Emptiness Checks for Generalized Büchi Automata" (Renault et al, LPAR 2013). Among the three emptiness checks that have been proposed, we opted to implement yGabow's one. More...
 
struct  ec_stats
 This structure contains, for each thread, the collected information during the traversal. More...
 
class  is_a_mc_algorithm
 This class allows to ensure (at compile time) if a given parameter can be compsidered as a modelchecking algorithm (i.e., usable by instanciate) More...
 
class  int_unionfind
 This Union-Find data structure is a particular union-find, dedicated for emptiness checks below, see ec.hh. The key of this union-find is int. Moreover, we suppose that only consecutive int are inserted. This union-find includes most of the classical optimisations (IPC, LR, PC, MS). More...
 
class  kripkecube_to_twa
 convert a (cube) model into a twa. Note that this algorithm cannot be run in parallel but could. More...
 
class  product_to_twa
 convert a (cube) product automaton into a twa Note that this algorithm cannot be run in parallel. More...
 
struct  bdd_less_than
 Comparison functor for BDDs. More...
 
struct  bdd_less_than_stable
 Comparison functor for BDDs. More...
 
struct  bdd_hash
 Hash functor for BDDs. More...
 
class  bitset
 
class  bitvect
 A bit vector. More...
 
class  bitvect_array
 
struct  parse_error
 
class  parallel_policy
 This class is used to tell parallel algorithms what resources they may use. More...
 
class  fixed_size_pool
 A fixed-size memory pool implementation. More...
 
class  printable
 
class  printable_value
 
class  printable_id
 The default callback simply writes "%c". More...
 
class  printable_percent
 Called by default for "%%" and "%\0". More...
 
class  formater
 
struct  ptr_hash
 A hash function for pointers. More...
 
struct  identity_hash
 A hash function that returns identity. More...
 
struct  pair_hash
 
struct  fnv
 Struct for Fowler-Noll-Vo parameters. More...
 
struct  fnv< T, typename std::enable_if< sizeof(T)==4 >::type >
 Fowler-Noll-Vo hash parameters for 32 bits. More...
 
struct  fnv< T, typename std::enable_if< sizeof(T)==8 >::type >
 Fowler-Noll-Vo hash parameters for 64 bits. More...
 
struct  char_ptr_less_than
 Strict Weak Ordering for char*. More...
 
class  minato_isop
 Generate an irredundant sum-of-products (ISOP) form of a BDD function. More...
 
class  multiple_size_pool
 A multiple-size memory pool implementation. More...
 
class  option_map
 Manage a map of options. More...
 
class  barand
 Compute pseudo-random integer value between 0 and n included, following a binomial distribution with probability p. More...
 
class  satsolver_command
 Interface with a given sat solver. More...
 
class  satsolver
 Interface with a SAT solver. More...
 
struct  stopwatch
 A simple stopwatch. More...
 
struct  time_info
 A structure to record elapsed time in clock ticks. More...
 
class  timer
 
class  timer_map
 A map of timer, where each timer has a name. More...
 
struct  process_timer
 Struct used to start and stop both timer and stopwatch clocks. More...
 
class  temporary_file
 Temporary file name. More...
 
class  open_temporary_file
 Open temporary file. More...
 
class  trival
 A class implementing Kleene's three-valued logic. More...
 
struct  hoa_abort
 
struct  parsed_aut
 Result of the automaton parser. More...
 
struct  automaton_parser_options
 
class  automaton_stream_parser
 Parse a stream of automata. More...
 
class  ta
 A Testing Automaton. More...
 
class  ta_succ_iterator
 Iterate over the successors of a state. More...
 
class  scc_stack_ta
 
class  ta_explicit
 
class  state_ta_explicit
 
class  ta_explicit_succ_iterator
 Successor iterators used by spot::ta_explicit. More...
 
class  state_ta_product
 A state for spot::ta_product. More...
 
class  ta_succ_iterator_product
 Iterate over the successors of a product computed on the fly. More...
 
class  ta_product
 A lazy product between a Testing automaton and a Kripke structure. (States are computed on the fly.) More...
 
class  ta_succ_iterator_product_by_changeset
 
class  tgta
 A Transition-based Generalized Testing Automaton (TGTA). More...
 
class  tgta_explicit
 
class  tgta_product
 A lazy product. (States are computed on the fly.) More...
 
class  tgta_succ_iterator_product
 Iterate over the successors of a product computed on the fly. More...
 
class  ta_check
 Check whether the language of a product (spot::ta_product) between a Kripke structure and a TA is empty. It works also for the product using Generalized TA (GTA and SGTA). More...
 
class  ta_reachable_iterator
 Iterate over all reachable states of a spot::ta. More...
 
class  ta_reachable_iterator_depth_first
 An implementation of spot::ta_reachable_iterator that browses states depth first. More...
 
class  ta_reachable_iterator_breadth_first
 An implementation of spot::ta_reachable_iterator that browses states breadth first. More...
 
struct  ta_statistics
 
class  language_containment_checker
 Check containment between LTL formulae. More...
 
class  declarative_environment
 A declarative environment. More...
 
class  default_environment
 A laxist environment. More...
 
class  environment
 An environment that describes atomic propositions. More...
 
class  exclusive_ap
 
class  fnode
 Actual storage for formula nodes. More...
 
struct  formula_ptr_less_than_bool_first
 
class  formula
 Main class for temporal logic formula. More...
 
class  mark_tools
 
struct  parsed_formula
 The result of a formula parser. More...
 
class  random_formula
 Base class for random formula generators. More...
 
class  random_ltl
 Generate random LTL formulae. More...
 
class  random_boolean
 Generate random Boolean formulae. More...
 
class  random_sere
 Generate random SERE. More...
 
class  random_psl
 Generate random PSL formulae. More...
 
class  randltlgenerator
 
class  tl_simplifier_options
 
class  tl_simplifier
 Rewrite or simplify f in various ways. More...
 
class  unabbreviator
 Clone and rewrite a formula to remove specified operators logical operators. More...
 
class  acc_cond
 An acceptance condition. More...
 
struct  rs_pairs_view
 
class  bdd_dict
 Map BDD variables to formulae. More...
 
class  taa_tgba
 A self-loop Transition-based Alternating Automaton (TAA) which is seen as a TGBA (abstract class, see below). More...
 
class  set_state
 Set of states deriving from spot::state. More...
 
class  taa_succ_iterator
 
class  taa_tgba_labelled
 
class  taa_tgba_string
 
class  taa_tgba_formula
 
class  state
 Abstract class for states. More...
 
struct  state_ptr_less_than
 Strict Weak Ordering for state*. More...
 
struct  state_ptr_equal
 An Equivalence Relation for state*. More...
 
struct  state_ptr_hash
 Hash Function for state*. More...
 
class  state_unicity_table
 Render state pointers unique via a hash table. More...
 
struct  state_shared_ptr_less_than
 Strict Weak Ordering for shared_state (shared_ptr<const state*>). More...
 
struct  state_shared_ptr_equal
 An Equivalence Relation for shared_state (shared_ptr<const state*>). More...
 
struct  state_shared_ptr_hash
 Hash Function for shared_state (shared_ptr<const state*>). More...
 
class  twa_succ_iterator
 Iterate over the successors of a state. More...
 
class  twa
 A Transition-based ω-Automaton. More...
 
struct  twa_graph_state
 Graph-based representation of a TωA. More...
 
struct  twa_graph_edge_data
 Data attached to edges of a twa_graph. More...
 
class  twa_graph_succ_iterator
 Iterator used by the on-the-fly interface of twa_graph. More...
 
class  twa_graph
 Graph-based representation of a TωA. More...
 
class  state_product
 A state for spot::twa_product. More...
 
class  twa_product
 A lazy product. (States are computed on the fly.) More...
 
class  twa_product_init
 A lazy product with different initial states. More...
 
class  aig
 A class representing AIG circuits. More...
 
class  isomorphism_checker
 Check if two automata are isomorphic. More...
 
class  bfs_steps
 Make a BFS in a spot::tgba to compute a twa_run::steps. More...
 
struct  nca_st_info
 
class  enumerate_cycles
 Enumerate elementary cycles in a SCC. More...
 
class  emptiness_check_result
 The result of an emptiness check. More...
 
class  emptiness_check
 Common interface to emptiness check algorithms. More...
 
class  emptiness_check_instantiator
 Dynamically create emptiness checks. Given their name and options. More...
 
struct  twa_run
 An accepted run, for a twa. More...
 
struct  unsigned_statistics
 
class  ec_statistics
 Emptiness-check statistics. More...
 
class  ars_statistics
 Accepting Run Search statistics. More...
 
class  acss_statistics
 Accepting Cycle Search Space statistics. More...
 
class  couvreur99_check_result
 Compute a counter example from a spot::couvreur99_check_status. More...
 
class  couvreur99_check
 An implementation of the Couvreur99 emptiness-check algorithm. More...
 
class  couvreur99_check_shy
 A version of spot::couvreur99_check that tries to visit known states first. More...
 
class  scc_stack
 
class  couvreur99_check_status
 The status of the emptiness-check on success. More...
 
class  hoa_alias_formater
 Help printing BDDs as text, using aliases. More...
 
struct  reduce_parity_data
 Internal data computed by the reduce_parity function. More...
 
class  postprocessor
 Wrap TGBA/BA/Monitor post-processing algorithms in an easy interface. More...
 
struct  power_map
 
class  output_aborter
 Helper object to specify when an algorithm should abort its construction. More...
 
class  twa_reachable_iterator
 Iterate over all reachable states of a spot::tgba. More...
 
class  twa_reachable_iterator_breadth_first
 An implementation of spot::twa_reachable_iterator that browses states breadth first. More...
 
class  twa_reachable_iterator_depth_first
 Iterate over all states of an automaton using a DFS. More...
 
class  twa_reachable_iterator_depth_first_stack
 Iterate over all states of an automaton using a DFS. More...
 
class  remove_ap
 
class  scc_info_node
 Storage for SCC related information. More...
 
class  scc_info
 Compute an SCC map and gather assorted information. More...
 
class  scc_and_mark_filter
 Create a filter for SCC and marks. More...
 
struct  twa_statistics
 
struct  twa_sub_statistics
 
class  printable_formula
 
class  printable_acc_cond
 
class  printable_scc_info
 
class  printable_size
 
class  printable_long_size
 
class  stat_printer
 prints various statistics about a TGBA More...
 
struct  synthesis_info
 Benchmarking data and options for synthesis. More...
 
struct  mealy_like
 A struct that represents different types of mealy like objects. More...
 
struct  to_parity_data
 
struct  to_parity_options
 Options to control various optimizations of to_parity(). More...
 
class  translator
 Translate an LTL formula into an optimized spot::tgba. More...
 
struct  twa_word
 An infinite word stored as a lasso. More...
 
class  zielonka_tree
 Zielonka Tree implementation. More...
 
class  acd
 Alternating Cycle Decomposition implementation. More...
 
class  cubeset
 
class  cstate
 Class for thread-safe states. More...
 
class  transition
 Class for representing a transition. More...
 
class  trans_index
 Class for iterators over transitions. More...
 
class  twacube
 Class for representing a thread-safe twa. More...
 

Typedefs

typedef std::shared_ptr< fair_kripkefair_kripke_ptr
 
typedef std::shared_ptr< const fair_kripkeconst_fair_kripke_ptr
 
typedef std::shared_ptr< kripkekripke_ptr
 
typedef std::shared_ptr< const kripkeconst_kripke_ptr
 
typedef std::shared_ptr< const kripke_explicit > const_kripke_explicit_ptr
 
typedef std::shared_ptr< kripke_explicit > kripke_explicit_ptr
 
typedef std::shared_ptr< kripke_graphkripke_graph_ptr
 
typedef struct spot::transition_info transition_info_t
 
typedef void(* TransitionCB) (void *ctx, transition_info_t *transition_info, int *dst)
 
using spins_interface_ptr = std::shared_ptr< const spins_interface >
 
typedef int * cspins_state
 A Spins state is represented as an array of integer Note that this array has two reserved slots (position 0 an 1). More...
 
typedef std::shared_ptr< spot::kripkecube< spot::cspins_state, spot::cspins_iterator > > ltsmin_kripkecube_ptr
 shortcut to manipulate the kripke below More...
 
typedef std::hash< std::string > string_hash
 A hash function for strings. More...
 
typedef std::pair< spot::location, std::string > parse_aut_error
 A parse diagnostic with its location. More...
 
typedef std::list< parse_aut_errorparse_aut_error_list
 A list of parser diagnostics, as filled by parse. More...
 
typedef std::shared_ptr< parsed_autparsed_aut_ptr
 
typedef std::shared_ptr< const parsed_autconst_parsed_aut_ptr
 
typedef std::shared_ptr< tata_ptr
 
typedef std::shared_ptr< const taconst_ta_ptr
 
typedef std::shared_ptr< ta_explicitta_explicit_ptr
 
typedef std::shared_ptr< const ta_explicitconst_ta_explicit_ptr
 
typedef std::shared_ptr< ta_productta_product_ptr
 
typedef std::shared_ptr< const ta_productconst_ta_product_ptr
 
typedef std::shared_ptr< tgtatgta_ptr
 
typedef std::shared_ptr< const tgtaconst_tgta_ptr
 
typedef std::shared_ptr< tgta_explicittgta_explicit_ptr
 
typedef std::shared_ptr< const tgta_explicitconst_tgta_explicit_ptr
 
typedef std::set< formulaatomic_prop_set
 Set of atomic propositions. More...
 
typedef std::pair< location, std::string > one_parse_error
 A parse diagnostic with its location. More...
 
typedef std::list< one_parse_errorparse_error_list
 A list of parser diagnostics, as filled by parse. More...
 
typedef std::map< formula, formularelabeling_map
 
typedef std::unordered_map< formula, formulasnf_cache
 
typedef std::shared_ptr< bdd_dictbdd_dict_ptr
 
typedef std::shared_ptr< twatwa_ptr
 
typedef std::shared_ptr< const twaconst_twa_ptr
 
typedef std::shared_ptr< const twa_graphconst_twa_graph_ptr
 
typedef std::shared_ptr< twa_graphtwa_graph_ptr
 
typedef std::shared_ptr< const twa_productconst_twa_product_ptr
 
typedef std::shared_ptr< twa_producttwa_product_ptr
 
typedef std::shared_ptr< taa_tgba_stringtaa_tgba_string_ptr
 
typedef std::shared_ptr< const taa_tgba_stringconst_taa_tgba_string_ptr
 
typedef std::shared_ptr< taa_tgba_formulataa_tgba_formula_ptr
 
typedef std::shared_ptr< const taa_tgba_formulaconst_taa_tgba_formula_ptr
 
typedef std::shared_ptr< twa_runtwa_run_ptr
 
typedef std::shared_ptr< twa_wordtwa_word_ptr
 
typedef std::unordered_set< const state *, state_ptr_hash, state_ptr_equalstate_set
 Unordered set of abstract states. More...
 
template<class val >
using state_map = std::unordered_map< const state *, val, state_ptr_hash, state_ptr_equal >
 Unordered map of abstract states. More...
 
typedef std::shared_ptr< const stateshared_state
 
typedef std::unordered_set< shared_state, state_shared_ptr_hash, state_shared_ptr_equalshared_state_set
 Unordered set of shared states. More...
 
typedef std::shared_ptr< aigaig_ptr
 
typedef std::shared_ptr< const aigconst_aig_ptr
 
typedef std::vector< struct nca_st_info * > vect_nca_info
 
typedef std::shared_ptr< const twa_runconst_twa_run_ptr
 
typedef std::shared_ptr< emptiness_check_resultemptiness_check_result_ptr
 
typedef std::shared_ptr< emptiness_checkemptiness_check_ptr
 
typedef std::shared_ptr< emptiness_check_instantiatoremptiness_check_instantiator_ptr
 
typedef std::vector< bool > region_t
 
typedef std::vector< unsigned > strategy_t
 
typedef std::vector< std::pair< unsigned, unsigned > > product_states
 Automata constructed by product() contain a property named "product-states" with this type. More...
 
using cube = unsigned *
 A cube is only a set of bits in memory. More...
 
typedef std::shared_ptr< twacubetwacube_ptr
 
typedef std::shared_ptr< const twacubeconst_twacube_ptr
 

Enumerations

enum class  mc_algorithm {
  BLOEMEN_EC , BLOEMEN_SCC , CNDFS , DEADLOCK ,
  REACHABILITY , SWARMING
}
 The list of parallel model-checking algorithms available. More...
 
enum class  mc_rvalue {
  DEADLOCK , EMPTY , FAILURE , NO_DEADLOCK ,
  NOT_EMPTY , SUCCESS
}
 
enum class  pool_type { Safe , Unsafe }
 
enum class  parsed_aut_type {
  HOA , NeverClaim , LBTT , DRA ,
  DSA , PGAME , Unknown
}
 
enum class  op : uint8_t {
  ff , tt , eword , ap ,
  Not , X , F , G ,
  Closure , NegClosure , NegClosureMarked , Xor ,
  Implies , Equiv , U , R ,
  W , M , EConcat , EConcatMarked ,
  UConcat , Or , OrRat , And ,
  AndRat , AndNLM , Concat , Fusion ,
  Star , FStar , first_match
}
 Operator types. More...
 
enum class  prcheck { Auto , via_CoBuchi , via_Rabin , via_Parity }
 Enum used to change the behavior of is_persistence() or is_recurrence(). More...
 
enum class  ocheck { Auto , via_CoBuchi , via_Rabin , via_WDBA }
 Enum used to change the behavior of is_obligation(). More...
 
enum  mut_opts {
  Mut_Ap2Const = 1U<<0 , Mut_Simplify_Bounds = 1U<<1 , Mut_Remove_Multop_Operands = 1U<<2 , Mut_Remove_Ops = 1U<<3 ,
  Mut_Split_Ops = 1U<<4 , Mut_Rewrite_Ops = 1U<<5 , Mut_Remove_One_Ap = 1U<<6 , Mut_All = -1U
}
 
enum  relabeling_style { Abc , Pnn }
 
enum class  scc_info_options {
  NONE = 0 , STOP_ON_ACC = 1 , TRACK_STATES = 2 , TRACK_SUCCS = 4 ,
  TRACK_STATES_IF_FIN_USED = 8 , ALL = TRACK_STATES | TRACK_SUCCS
}
 Options to alter the behavior of scc_info. More...
 
enum class  zielonka_tree_options {
  NONE = 0 , CHECK_RABIN = 1 , CHECK_STREETT = 2 , CHECK_PARITY = CHECK_RABIN | CHECK_STREETT ,
  ABORT_WRONG_SHAPE = 4 , MERGE_SUBTREES = 8
}
 Options to alter the behavior of acd. More...
 
enum class  acd_options {
  NONE = 0 , CHECK_RABIN = 1 , CHECK_STREETT = 2 , CHECK_PARITY = CHECK_RABIN | CHECK_STREETT ,
  ABORT_WRONG_SHAPE = 4 , ORDER_HEURISTIC = 8
}
 Options to alter the behavior of acd. More...
 

Functions

kripke_graph_ptr make_kripke_graph (const bdd_dict_ptr &d)
 
std::ostream & operator<< (std::ostream &os, const mc_algorithm &ma)
 
std::ostream & operator<< (std::ostream &os, const mc_rvalue &mr)
 
std::ostream & operator<< (std::ostream &os, const ec_stats &es)
 
const mc_rvalue operator| (const mc_rvalue &lhs, const mc_rvalue &rhs)
 This function helps to find the output value from a set of threads that may have different values. More...
 
template<typename T , typename U >
down_cast (U *u) noexcept
 
template<typename T , typename U >
down_cast (const std::shared_ptr< U > &u) noexcept
 
template<typename T , typename U >
down_cast (U u)
 
template<typename Type , typename = std::enable_if_t<std::is_unsigned<Type>::value>>
constexpr unsigned clz (Type n) noexcept
 
int memusage ()
 Total number of pages in use by the program. More...
 
const char * version ()
 Return Spot's version. More...
 
void hoayyreset (void *scanner)
 
int hoayyopen (const std::string &name, void **scanner)
 
int hoayyopen (int fd, void **scanner)
 
int hoayystring (const char *data, void **scanner)
 
void hoayyclose (void *scanner)
 
parsed_aut_ptr parse_aut (const std::string &filename, const bdd_dict_ptr &dict, environment &env=default_environment::instance(), automaton_parser_options opts={})
 Read the first spot::twa_graph from a file. More...
 
ta_explicit_ptr make_ta_explicit (const const_twa_ptr &tgba, unsigned n_acc, state_ta_explicit *artificial_initial_state=nullptr)
 
ta_product_ptr product (const const_ta_ptr &testing_automaton, const const_kripke_ptr &kripke_structure)
 
tgta_explicit_ptr make_tgta_explicit (const const_twa_ptr &tgba, unsigned n_acc, state_ta_explicit *artificial_initial_state=nullptr)
 
twa_ptr product (const const_kripke_ptr &left, const const_tgta_ptr &right)
 
std::ostream & print_dot (std::ostream &os, const const_ta_ptr &a, const char *opt=nullptr)
 
ta_explicit_ptr minimize_ta (const const_ta_ptr &ta_)
 Construct a simplified TA by merging bisimilar states. More...
 
tgta_explicit_ptr minimize_tgta (const const_tgta_explicit_ptr &tgta_)
 Construct a simplified TGTA by merging bisimilar states. More...
 
std::set< const state * > get_states_set (const const_ta_ptr &t)
 Compute states set for an automaton. More...
 
ta_statistics stats_reachable (const const_ta_ptr &t)
 Compute statistics for an automaton. More...
 
ta_explicit_ptr tgba_to_ta (const const_twa_ptr &tgba_to_convert, bdd atomic_propositions_set, bool degeneralized=true, bool artificial_initial_state_mode=true, bool single_pass_emptiness_check=false, bool artificial_livelock_state_mode=false, bool no_livelock=false)
 Build a spot::ta_explicit* (TA) from an LTL formula. More...
 
tgta_explicit_ptr tgba_to_tgta (const const_twa_ptr &tgba_to_convert, bdd atomic_propositions_set)
 Build a spot::tgta_explicit* (TGTA) from an LTL formula. More...
 
atomic_prop_set create_atomic_prop_set (unsigned n)
 construct an atomic_prop_set with n propositions More...
 
atomic_prop_setatomic_prop_collect (formula f, atomic_prop_set *s=nullptr)
 Return the set of atomic propositions occurring in a formula. More...
 
bdd atomic_prop_collect_as_bdd (formula f, const twa_ptr &a)
 Return the set of atomic propositions occurring in a formula, as a BDD. More...
 
std::ostream & print_dot_psl (std::ostream &os, formula f)
 Write a formula tree using dot's syntax. More...
 
int atomic_prop_cmp (const fnode *f, const fnode *g)
 Order two atomic propositions. More...
 
std::ostream & print_formula_props (std::ostream &out, const formula &f, bool abbreviated=false)
 Print the properties of formula f on stream out. More...
 
std::list< std::string > list_formula_props (const formula &f)
 List the properties of formula f. More...
 
std::ostream & operator<< (std::ostream &os, const formula &f)
 Print a formula. More...
 
bool is_persistence (formula f, twa_graph_ptr aut=nullptr, prcheck algo=prcheck::Auto)
 Return true if f represents a persistence property. More...
 
bool is_recurrence (formula f, twa_graph_ptr aut=nullptr, prcheck algo=prcheck::Auto)
 Return true if f represents a recurrence property. More...
 
bool is_obligation (formula f, twa_graph_ptr aut=nullptr, ocheck algo=ocheck::Auto)
 Return true if f has the recurrence property. More...
 
char mp_class (formula f)
 Return the class of f in the temporal hierarchy of Manna and Pnueli (PODC'90). More...
 
std::string mp_class (formula f, const char *opt)
 Return the class of f in the temporal hierarchy of Manna and Pnueli (PODC'90). More...
 
std::string mp_class (char mpc, const char *opt)
 Expand a class in the temporal hierarchy of Manna and Pnueli (PODC'90). More...
 
unsigned nesting_depth (formula f, op oper)
 Compute the nesting depth of an operator. More...
 
unsigned nesting_depth (formula f, const op *begin, const op *end)
 Compute the nesting depth of a set of operators. More...
 
unsigned nesting_depth (formula f, const char *opers)
 Compute the nesting depth of a set of operators. More...
 
bool is_liveness (formula f)
 Check whether a formula represents a liveness property. More...
 
int length (formula f)
 Compute the length of a formula. More...
 
int length_boolone (formula f)
 Compute the length of a formula, squashing Boolean formulae. More...
 
formula from_ltlf (formula f, const char *alive="alive")
 Convert an LTLf into an LTL formula. More...
 
std::vector< formulamutate (formula f, unsigned opts=Mut_All, unsigned max_output=-1U, unsigned mutation_count=1, bool sort=true)
 
formula negative_normal_form (formula f, bool negated=false)
 Build the negative normal form of f. More...
 
parsed_formula parse_infix_psl (const std::string &ltl_string, environment &env=default_environment::instance(), bool debug=false, bool lenient=false)
 Build a formula from an LTL string. More...
 
parsed_formula parse_infix_boolean (const std::string &ltl_string, environment &env=default_environment::instance(), bool debug=false, bool lenient=false)
 Build a Boolean formula from a string. More...
 
parsed_formula parse_prefix_ltl (const std::string &ltl_string, environment &env=default_environment::instance(), bool debug=false)
 Build a formula from an LTL string in LBT's format. More...
 
formula parse_formula (const std::string &ltl_string, environment &env=default_environment::instance())
 A simple wrapper to parse_infix_psl() and parse_prefix_ltl(). More...
 
parsed_formula parse_infix_sere (const std::string &sere_string, environment &env=default_environment::instance(), bool debug=false, bool lenient=false)
 Build a formula from a string representing a SERE. More...
 
void fix_utf8_locations (const std::string &input_string, parse_error_list &error_list)
 Fix location of diagnostics assuming the input is utf8. More...
 
std::ostream & print_psl (std::ostream &os, formula f, bool full_parent=false)
 Output a PSL formula as a string which is parsable. More...
 
std::string str_psl (formula f, bool full_parent=false)
 Convert a PSL formula into a string which is parsable. More...
 
std::ostream & print_utf8_psl (std::ostream &os, formula f, bool full_parent=false)
 Output a PSL formula as an utf-8 string which is parsable. More...
 
std::string str_utf8_psl (formula f, bool full_parent=false)
 Convert a PSL formula into a utf-8 string which is parsable. More...
 
std::ostream & print_sere (std::ostream &os, formula f, bool full_parent=false)
 Output a SERE formula as a string which is parsable. More...
 
std::string str_sere (formula f, bool full_parent=false)
 Convert a SERE formula into a string which is parsable. More...
 
std::ostream & print_utf8_sere (std::ostream &os, formula f, bool full_parent=false)
 Output a SERE formula as a utf-8 string which is parsable. More...
 
std::string str_utf8_sere (formula f, bool full_parent=false)
 Convert a SERE formula into a string which is parsable. More...
 
std::ostream & print_spin_ltl (std::ostream &os, formula f, bool full_parent=false)
 Output an LTL formula as a string parsable by Spin. More...
 
std::string str_spin_ltl (formula f, bool full_parent=false)
 Convert an LTL formula into a string parsable by Spin. More...
 
std::ostream & print_wring_ltl (std::ostream &os, formula f)
 Output an LTL formula as a string parsable by Wring. More...
 
std::string str_wring_ltl (formula f)
 Convert a formula into a string parsable by Wring. More...
 
std::ostream & print_latex_psl (std::ostream &os, formula f, bool full_parent=false)
 Output a PSL formula as a LaTeX string. More...
 
std::string str_latex_psl (formula f, bool full_parent=false)
 Output a formula as a LaTeX string which is parsable. unless the formula contains automaton operators (used in ELTL formulae). More...
 
std::ostream & print_latex_sere (std::ostream &os, formula f, bool full_parent=false)
 Output a SERE formula as a LaTeX string. More...
 
std::string str_latex_sere (formula f, bool full_parent=false)
 Output a SERE formula as a LaTeX string which is parsable. unless the formula contains automaton operators (used in ELTL formulae). More...
 
std::ostream & print_sclatex_psl (std::ostream &os, formula f, bool full_parent=false)
 Output a PSL formula as a self-contained LaTeX string. More...
 
std::string str_sclatex_psl (formula f, bool full_parent=false)
 Output a PSL formula as a self-contained LaTeX string. More...
 
std::ostream & print_sclatex_sere (std::ostream &os, formula f, bool full_parent=false)
 Output a SERE formula as a self-contained LaTeX string. More...
 
std::string str_sclatex_sere (formula f, bool full_parent=false)
 Output a SERE formula as a self-contained LaTeX string. More...
 
std::ostream & print_lbt_ltl (std::ostream &os, formula f)
 Output an LTL formula as a string in LBT's format. More...
 
std::string str_lbt_ltl (formula f)
 Output an LTL formula as a string in LBT's format. More...
 
formula relabel (formula f, relabeling_style style, relabeling_map *m=nullptr)
 Relabel the atomic propositions in a formula. More...
 
formula relabel_bse (formula f, relabeling_style style, relabeling_map *m=nullptr)
 Relabel Boolean subexpressions in a formula using atomic propositions. More...
 
formula relabel_apply (formula f, relabeling_map *m)
 Replace atomic propositions of f by subformulas specified in m. More...
 
formula remove_x (formula f)
 Rewrite a stutter-insensitive formula f without using the X operator. More...
 
formula star_normal_form (formula sere, snf_cache *cache=nullptr)
 Helper to rewrite a sere in Star Normal Form. More...
 
formula star_normal_form_bounded (formula sere, snf_cache *cache=nullptr)
 A variant of star_normal_form() for r[*0..j] where j < ω. More...
 
std::pair< formula, std::vector< std::string > > suffix_operator_normal_form (formula f, const std::string prefix)
 Helper to rewrite a PSL formula in Suffix Operator Normal Form. More...
 
formula unabbreviate (formula in, const char *opt=default_unabbrev_string)
 Clone and rewrite a formula to remove specified operators logical operators. More...
 
bdd_dict_ptr make_bdd_dict ()
 
std::ostream & bdd_print_sat (std::ostream &os, const bdd_dict_ptr &dict, bdd b)
 Print a BDD as a list of literals. More...
 
std::string bdd_format_sat (const bdd_dict_ptr &dict, bdd b)
 Format a BDD as a list of literals. More...
 
std::ostream & bdd_print_accset (std::ostream &os, const bdd_dict_ptr &dict, bdd b)
 Print a BDD as a set of acceptance conditions. More...
 
std::string bdd_format_accset (const bdd_dict_ptr &dict, bdd b)
 Format a BDD as a set of acceptance conditions. More...
 
std::ostream & bdd_print_set (std::ostream &os, const bdd_dict_ptr &dict, bdd b)
 Print a BDD as a set. More...
 
std::string bdd_format_set (const bdd_dict_ptr &dict, bdd b)
 Format a BDD as a set. More...
 
std::ostream & bdd_print_formula (std::ostream &os, const bdd_dict_ptr &dict, bdd b)
 Print a BDD as a formula. More...
 
std::string bdd_format_formula (const bdd_dict_ptr &dict, bdd b)
 Format a BDD as a formula. More...
 
void enable_utf8 ()
 Enable UTF-8 output for bdd printers. More...
 
std::string bdd_format_isop (const bdd_dict_ptr &dict, bdd b)
 Format a BDD as an irredundant sum of product. More...
 
std::ostream & bdd_print_isop (std::ostream &os, const bdd_dict_ptr &dict, bdd b)
 Print a BDD as an irredundant sum of product. More...
 
formula bdd_to_formula (bdd f, const bdd_dict_ptr d)
 Convert a BDD into a formula. More...
 
taa_tgba_string_ptr make_taa_tgba_string (const bdd_dict_ptr &dict)
 
taa_tgba_formula_ptr make_taa_tgba_formula (const bdd_dict_ptr &dict)
 
void shared_state_deleter (state *s)
 
void prop_copy (const const_twa_ptr &other, prop_set p)
 Copy the properties of another automaton. More...
 
void prop_keep (prop_set p)
 Keep only a subset of properties of the current automaton. More...
 
void prop_reset ()
 
twa_graph_ptr make_twa_graph (const bdd_dict_ptr &dict)
 Build an explicit automaton from all states of aut,. More...
 
twa_graph_ptr make_twa_graph (const twa_graph_ptr &aut, twa::prop_set p)
 Build an explicit automaton from all states of aut,. More...
 
twa_graph_ptr make_twa_graph (const const_twa_graph_ptr &aut, twa::prop_set p, bool preserve_name_properties=false)
 Clone a twa_graph. More...
 
twa_graph_ptr make_twa_graph (const const_twa_ptr &aut, twa::prop_set p, bool preserve_names=false, unsigned max_states=-(1U))
 Build an explicit automaton from all states of aut,. More...
 
twa_product_ptr otf_product (const const_twa_ptr &left, const const_twa_ptr &right)
 on-the-fly TGBA product More...
 
twa_product_ptr otf_product_at (const const_twa_ptr &left, const const_twa_ptr &right, const state *left_init, const state *right_init)
 on-the-fly TGBA product with forced initial states More...
 
std::ostream & print_aiger (std::ostream &os, const_aig_ptr circuit)
 Print the aig to stream in AIGER format. More...
 
std::ostream & print_aiger (std::ostream &os, const const_twa_graph_ptr &aut, const char *mode)
 Encode and print an automaton as an AIGER circuit. More...
 
twa_graph_ptr canonicalize (twa_graph_ptr aut)
 Reorder the states and transitions of aut in a way that will be the same for every isomorphic automata. More...
 
twa_graph_ptr nsa_to_nca (const_twa_graph_ptr aut, bool named_states=false, vect_nca_info *nca_info=nullptr)
 Converts a nondet Streett-like aut. to a nondet. co-Büchi aut. More...
 
twa_graph_ptr dnf_to_nca (const_twa_graph_ptr aut, bool named_states=false, vect_nca_info *nca_info=nullptr)
 Converts an aut. with acceptance in DNF to a nondet. co-Büchi aut. More...
 
twa_graph_ptr to_nca (const_twa_graph_ptr aut, bool named_states=false)
 Converts any ω-automata to non-deterministic co-buchi. More...
 
twa_graph_ptr nsa_to_dca (const_twa_graph_ptr aut, bool named_states=false)
 Converts a nondet Streett-like aut. to a det. co-Büchi aut. More...
 
twa_graph_ptr dnf_to_dca (const_twa_graph_ptr aut, bool named_states=false)
 Converts an aut. with acceptance in DNF to a det. co-Büchi aut. More...
 
twa_graph_ptr to_dca (const_twa_graph_ptr aut, bool named_states=false)
 Converts any ω-automata to deterministic co-buchi. More...
 
twa_graph_ptr dtwa_complement (const const_twa_graph_ptr &aut)
 Complement a deterministic TωA. More...
 
twa_graph_ptr complement_semidet (const const_twa_graph_ptr &aut, bool show_names=false)
 Complement a semideterministic TωA. More...
 
twa_graph_ptr complement (const const_twa_graph_ptr &aut, const output_aborter *aborter=nullptr)
 Complement a TωA. More...
 
void complete_here (twa_graph_ptr aut)
 Complete a twa_graph in place. More...
 
twa_graph_ptr complete (const const_twa_ptr &aut)
 Clone a twa and complete it. More...
 
twa_graph_ptr compsusp (formula f, const bdd_dict_ptr &dict, bool no_wdba=false, bool no_simulation=false, bool early_susp=false, bool no_susp_product=false, bool wdba_smaller=false, bool oblig=false)
 Compositional translation algorithm with resetable suspension. More...
 
twa_graph_ptr copy (const const_twa_ptr &aut, twa::prop_set p, bool preserve_names=false, unsigned max_states=-1U)
 Build an explicit automaton from all states of aut,. More...
 
emptiness_check_ptr get_couvreur99_new (const const_twa_ptr &a, option_map o)
 A rewritten version of the Couvreur emptiness check. More...
 
emptiness_check_ptr get_couvreur99_new_abstract (const const_twa_ptr &a, option_map o)
 Same as above, but always uses the abstract interface. More...
 
emptiness_check_result_ptr couvreur99_new_check (const const_twa_ptr &a)
 A shortcut to run the optimized emptiness check directly. More...
 
bool delay_branching_here (const twa_graph_ptr &aut)
 Merge states to delay. More...
 
twa_graph_ptr degeneralize (const const_twa_graph_ptr &a, bool use_z_lvl=true, bool use_cust_acc_orders=false, int use_lvl_cache=1, bool skip_levels=true, bool ignaccsl=false, bool remove_extra_scc=true)
 Degeneralize a generalized (co)Büchi automaton into an equivalent (co)Büchi automaton. More...
 
twa_graph_ptr degeneralize_tba (const const_twa_graph_ptr &a, bool use_z_lvl=true, bool use_cust_acc_orders=false, int use_lvl_cache=1, bool skip_levels=true, bool ignaccsl=false, bool remove_extra_scc=true)
 
acc_cond::mark_t is_partially_degeneralizable (const const_twa_graph_ptr &aut, bool allow_inf=true, bool allow_fin=true, std::vector< acc_cond::mark_t > forbid={})
 Is the automaton partially degeneralizable? More...
 
twa_graph_ptr tgba_determinize (const const_twa_graph_ptr &aut, bool pretty_print=false, bool use_scc=true, bool use_simulation=true, bool use_stutter=true, const output_aborter *aborter=nullptr, int trans_pruning=-1, bool want_classes=false)
 Determinize a TGBA. More...
 
std::ostream & print_dot (std::ostream &os, const const_twa_ptr &g, const char *options=nullptr)
 Print reachable states in dot format. More...
 
std::ostream & print_dot (std::ostream &os, aig_ptr circuit, const char *=nullptr)
 
twa_graph_ptr dtba_sat_synthetize (const const_twa_graph_ptr &a, int target_state_number, bool state_based=false)
 Attempt to synthetize an equivalent deterministic TBA with a SAT solver. More...
 
twa_graph_ptr dtba_sat_minimize (const const_twa_graph_ptr &a, bool state_based=false, int max_states=-1)
 Attempt to minimize a deterministic TBA with a SAT solver. More...
 
twa_graph_ptr dtba_sat_minimize_dichotomy (const const_twa_graph_ptr &a, bool state_based=false, bool langmap=false, int max_states=-1)
 Attempt to minimize a deterministic TBA with a SAT solver. More...
 
twa_graph_ptr dtba_sat_minimize_incr (const const_twa_graph_ptr &a, bool state_based=false, int max_states=-1, int param=2)
 Attempt to minimize a det. TBA with a SAT solver. More...
 
twa_graph_ptr dtba_sat_minimize_assume (const const_twa_graph_ptr &a, bool state_based=false, int max_states=-1, int param=6)
 Attempt to minimize a deterministic TBA incrementally with a SAT solver. More...
 
twa_graph_ptr dtwa_sat_synthetize (const const_twa_graph_ptr &a, unsigned target_acc_number, const acc_cond::acc_code &target_acc, int target_state_number, bool state_based=false, bool colored=false)
 Attempt to synthetize an equivalent deterministic TωA with a SAT solver. More...
 
twa_graph_ptr dtwa_sat_minimize (const const_twa_graph_ptr &a, unsigned target_acc_number, const acc_cond::acc_code &target_acc, bool state_based=false, int max_states=-1, bool colored=false)
 Attempt to minimize a deterministic TωA with a SAT solver. More...
 
twa_graph_ptr dtwa_sat_minimize_dichotomy (const const_twa_graph_ptr &a, unsigned target_acc_number, const acc_cond::acc_code &target_acc, bool state_based=false, bool langmap=false, int max_states=-1, bool colored=false)
 Attempt to minimize a deterministic TωA with a SAT solver. More...
 
twa_graph_ptr dtwa_sat_minimize_incr (const const_twa_graph_ptr &a, unsigned target_acc_number, const acc_cond::acc_code &target_acc, bool state_based=false, int max_states=-1, bool colored=false, int param=2)
 Attempt to minimize a deterministic TωA with a SAT solver. More...
 
twa_graph_ptr dtwa_sat_minimize_assume (const const_twa_graph_ptr &a, unsigned target_acc_number, const acc_cond::acc_code &target_acc, bool state_based=false, int max_states=-1, bool colored=false, int param=6)
 Attempt to minimize a deterministic TωA with a SAT solver. More...
 
twa_graph_ptr sat_minimize (twa_graph_ptr aut, const char *opt, bool state_based=false)
 High-level interface to SAT-based minimization. More...
 
twa_graph_ptr dualize (const const_twa_graph_ptr &aut)
 Complement an automaton by dualizing it. More...
 
emptiness_check_instantiator_ptr make_emptiness_check_instantiator (const char *name, const char **err)
 Create an emptiness-check instantiator, given the name of an emptiness check. More...
 
void alternate_players (spot::twa_graph_ptr &arena, bool first_player=false, bool complete0=true)
 Transform an automaton into a parity game by propagating players. More...
 
bool solve_parity_game (const twa_graph_ptr &arena)
 solve a parity-game More...
 
bool solve_safety_game (const twa_graph_ptr &game)
 Solve a safety game. More...
 
bool solve_game (const twa_graph_ptr &arena)
 Generic interface for game solving. More...
 
twa_graph_ptr highlight_strategy (twa_graph_ptr &arena, int player0_color=5, int player1_color=4)
 Highlight the edges of a strategy on an automaton. More...
 
void set_state_player (twa_graph_ptr arena, unsigned state, bool owner)
 Set the owner of a state. More...
 
bool get_state_player (const_twa_graph_ptr arena, unsigned state)
 Get the owner of a state. More...
 
const region_t & get_state_players (const_twa_graph_ptr arena)
 Get the owner of all states. More...
 
void set_synthesis_outputs (const twa_graph_ptr &arena, const bdd &outs)
 Set all synthesis outputs as a conjunction. More...
 
bdd get_synthesis_outputs (const const_twa_graph_ptr &arena)
 Get all synthesis outputs as a conjunction. More...
 
std::vector< std::string > get_synthesis_output_aps (const const_twa_graph_ptr &arena)
 Get the vector with the names of the output propositions. More...
 
void set_state_winner (twa_graph_ptr arena, unsigned state, bool winner)
 Set the winner of a state. More...
 
bool get_state_winner (const_twa_graph_ptr arena, unsigned state)
 Get the winner of a state. More...
 
const region_t & get_state_winners (const_twa_graph_ptr arena)
 Get the winner of all states. More...
 
bool generic_emptiness_check (const const_twa_graph_ptr &aut)
 Emptiness check of an automaton, for any acceptance condition. More...
 
twa_run_ptr generic_accepting_run (const const_twa_graph_ptr &aut)
 Accepting run search in an automaton, for any acceptance condition. More...
 
bool generic_emptiness_check_for_scc (const scc_info &si, unsigned scc)
 Emptiness check of one SCC, for any acceptance condition. More...
 
bool generic_emptiness_check_for_scc (const scc_info &si, unsigned scc, const acc_cond &forced_acc)
 Emptiness check of one SCC, for any acceptance condition. More...
 
bool maximal_accepting_loops_for_scc (const scc_info &si, unsigned scc, const acc_cond &forced_acc, const bitvect &keep, std::function< void(const scc_info &, unsigned)> callback)
 Compute set of maximal accepting loops in one SCC, for any acceptance condition. More...
 
void generic_emptiness_check_select_version (const char *emversion=nullptr)
 
bool accepting_transitions_scc (const scc_info &si, unsigned scc, const acc_cond aut_acc, acc_cond::mark_t removed_colors, std::vector< bool > &accepting_transitions, const bitvect &kept)
 
std::vector< bool > accepting_transitions (const const_twa_graph_ptr aut, acc_cond cond)
 
twa_graph_ptr g_f_terminal_inplace (twa_graph_ptr f_terminal, bool state_based=false)
 Given a terminal automaton f_terminal recognizing some formula F(φ), modify it to recognize GF(φ). More...
 
twa_graph_ptr gf_guarantee_to_ba_maybe (formula gf, const bdd_dict_ptr &dict, bool deterministic=true, bool state_based=false)
 Convert GF(φ) into a (D)BA if φ is a guarantee property. More...
 
twa_graph_ptr gf_guarantee_to_ba (formula gf, const bdd_dict_ptr &dict, bool deterministic=true, bool state_based=false)
 Convert GF(φ) into a (D)BA if φ is a guarantee property. More...
 
twa_graph_ptr fg_safety_to_dca_maybe (formula fg, const bdd_dict_ptr &dict, bool state_based)
 Convert FG(φ) into a DCA if φ is a safety property. More...
 
twa_graph_ptr fg_safety_to_dca (formula fg, const bdd_dict_ptr &dict, bool state_based=false)
 Convert FG(φ) into a DCA if φ is a safety property. More...
 
emptiness_check_ptr couvreur99 (const const_twa_ptr &a, option_map options=option_map())
 Check whether the language of an automate is empty. More...
 
emptiness_check_ptr explicit_gv04_check (const const_twa_ptr &a, option_map o=option_map())
 Emptiness check based on Geldenhuys and Valmari's TACAS'04 paper. More...
 
std::ostream & print_hoa (std::ostream &os, const const_twa_ptr &g, const char *opt=nullptr)
 Print reachable states in Hanoi Omega Automata format. More...
 
std::vector< std::pair< std::string, bdd > > * get_aliases (const const_twa_ptr &g)
 Obtain aliases used in the HOA format. More...
 
void set_aliases (twa_ptr g, std::vector< std::pair< std::string, bdd >> aliases)
 Define all aliases used in the HOA format. More...
 
bool is_colored (const const_twa_graph_ptr &aut)
 Return true iff aut is colored. More...
 
unsigned count_nondet_states (const const_twa_graph_ptr &aut)
 Count the number of states with non-deterministic branching in aut. More...
 
bool is_universal (const const_twa_graph_ptr &aut)
 Return true iff aut is universal. More...
 
bool is_deterministic (const const_twa_graph_ptr &aut)
 Return true iff aut is deterministic. More...
 
void highlight_nondet_states (twa_graph_ptr &aut, unsigned color)
 Highlight nondeterministic states. More...
 
void highlight_nondet_edges (twa_graph_ptr &aut, unsigned color)
 Highlight nondeterministic edges. More...
 
void highlight_semidet_sccs (scc_info &si, unsigned color)
 Highlight the deterministic part of the automaton. More...
 
bool is_complete (const const_twa_graph_ptr &aut)
 Return true iff aut is complete. More...
 
bool is_semi_deterministic (const const_twa_graph_ptr &aut)
 Return true iff aut is semi-deterministic. More...
 
std::vector< bool > semidet_sccs (scc_info &si)
 Whether an SCC is in the deterministic part of an automaton. More...
 
void check_determinism (twa_graph_ptr aut)
 Set the deterministic and semi-deterministic properties appropriately. More...
 
unsigned count_univbranch_states (const const_twa_graph_ptr &aut)
 
unsigned count_univbranch_edges (const const_twa_graph_ptr &aut)
 
bool is_unambiguous (const const_twa_graph_ptr &aut)
 Whether the automaton aut is unambiguous. More...
 
bool check_unambiguous (const twa_graph_ptr &aut)
 Like is_unambiguous(), but also sets the property in the twa. More...
 
bool scc_has_rejecting_cycle (scc_info &map, unsigned scc)
 Whether the SCC number scc in map has a rejecting cycle. More...
 
bool is_inherently_weak_scc (scc_info &map, unsigned scc)
 Whether the SCC number scc in map is inherently weak. More...
 
bool is_weak_scc (scc_info &map, unsigned scc)
 Whether the SCC number scc in map is weak. More...
 
bool is_complete_scc (scc_info &map, unsigned scc)
 Whether the SCC number scc in map is complete. More...
 
bool is_terminal_scc (scc_info &map, unsigned scc)
 Whether the SCC number scc in map is terminal. More...
 
std::vector< unsigned > language_map (const const_twa_graph_ptr &aut)
 Identify states that recognize the same language. More...
 
void highlight_languages (twa_graph_ptr &aut)
 Color state that recognize identical language. More...
 
std::ostream & print_lbtt (std::ostream &os, const const_twa_ptr &g, const char *opt=nullptr)
 Print reachable states in LBTT's format. More...
 
taa_tgba_formula_ptr ltl_to_taa (formula f, const bdd_dict_ptr &dict, bool refined_rules=false)
 Build a spot::taa* from an LTL formula. More...
 
twa_graph_ptr ltl_to_tgba_fm (formula f, const bdd_dict_ptr &dict, bool exprop=false, bool symb_merge=true, bool branching_postponement=false, bool fair_loop_approx=false, const atomic_prop_set *unobs=nullptr, tl_simplifier *simplifier=nullptr, bool unambiguous=false, const output_aborter *aborter=nullptr)
 Build a spot::twa_graph_ptr from an LTL or PSL formula. More...
 
emptiness_check_ptr explicit_magic_search (const const_twa_ptr &a, option_map o=option_map())
 Returns an emptiness checker on the spot::tgba automaton a. More...
 
emptiness_check_ptr bit_state_hashing_magic_search (const const_twa_ptr &a, size_t size, option_map o=option_map())
 Returns an emptiness checker on the spot::tgba automaton a. More...
 
emptiness_check_ptr magic_search (const const_twa_ptr &a, option_map o=option_map())
 Wrapper for the two magic_search implementations. More...
 
template<typename Trans >
void transform_accessible (const const_twa_graph_ptr &old, twa_graph_ptr &cpy, Trans trans, unsigned int init, bool drop_univ_branches=false)
 Clone and mask an automaton. More...
 
template<typename Trans >
void transform_copy (const const_twa_graph_ptr &old, twa_graph_ptr &cpy, Trans trans, unsigned int init)
 Copy an automaton and update each edge. More...
 
template<typename Trans >
void transform_accessible (const const_twa_graph_ptr &old, twa_graph_ptr &cpy, Trans trans)
 
template<typename Trans >
void transform_copy (const const_twa_graph_ptr &old, twa_graph_ptr &cpy, Trans trans)
 
twa_graph_ptr mask_acc_sets (const const_twa_graph_ptr &in, acc_cond::mark_t to_remove)
 Remove all edges that belong to some given acceptance sets. More...
 
twa_graph_ptr mask_keep_states (const const_twa_graph_ptr &in, std::vector< bool > &to_keep, unsigned int init)
 Keep only the states as specified by to_keep. More...
 
twa_graph_ptr mask_keep_accessible_states (const const_twa_graph_ptr &in, std::vector< bool > &to_keep, unsigned int init, bool drop_univ_branches=false)
 Keep only the states specified by to_keep that are accessible. More...
 
bool is_mealy (const const_twa_graph_ptr &m)
 Checks whether the automaton is a mealy machine. More...
 
bool is_separated_mealy (const const_twa_graph_ptr &m)
 Checks whether the automaton is a separated mealy machine. More...
 
bool is_split_mealy (const const_twa_graph_ptr &m)
 Checks whether or not the automaton is a split mealy machine. More...
 
bool is_input_deterministic_mealy (const const_twa_graph_ptr &m)
 Checks whether a mealy machine is input deterministic. More...
 
twa_graph_ptr unsplit_mealy (const const_twa_graph_ptr &m)
 the inverse of split_separated_mealy More...
 
twa_graph_ptr minimize_mealy (const const_twa_graph_ptr &mm, int premin=-1)
 Minimizes an (in)completely specified mealy machine. More...
 
twa_graph_ptr minimize_mealy (const const_twa_graph_ptr &mm, synthesis_info &si)
 Minimizes an (in)completely specified mealy machine. More...
 
bool is_split_mealy_specialization (const_twa_graph_ptr left, const_twa_graph_ptr right, bool verbose=false)
 Test if the split mealy machine right is a specialization of the split mealy machine left. More...
 
twa_graph_ptr mealy_product (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
 Product between two mealy machines left and right. More...
 
twa_graph_ptr minimize_monitor (const const_twa_graph_ptr &a)
 Construct a minimal deterministic monitor. More...
 
twa_graph_ptr minimize_wdba (const const_twa_graph_ptr &a, const output_aborter *aborter=nullptr)
 Minimize a Büchi automaton in the WDBA class. More...
 
twa_graph_ptr minimize_obligation (const const_twa_graph_ptr &aut_f, formula f=nullptr, const_twa_graph_ptr aut_neg_f=nullptr, bool reject_bigger=false, const output_aborter *aborter=nullptr)
 Minimize an automaton if it represents an obligation property. More...
 
bool minimize_obligation_garanteed_to_work (const const_twa_graph_ptr &aut_f, formula f=nullptr)
 Whether calling minimize_obligation is sure to work. More...
 
std::ostream & print_never_claim (std::ostream &os, const const_twa_ptr &g, const char *opt=nullptr)
 Print reachable states in Spin never claim format. More...
 
twa_graph_ptr tgba_powerset (const const_twa_graph_ptr &aut, power_map &pm, bool merge=true, const output_aborter *aborter=nullptr, std::vector< unsigned > *accepting_sinks=nullptr)
 Build a deterministic automaton, ignoring acceptance conditions. More...
 
twa_graph_ptr tgba_powerset (const const_twa_graph_ptr &aut, const output_aborter *aborter=nullptr, std::vector< unsigned > *accepting_sinks=nullptr)
 
twa_graph_ptr tba_determinize (const const_twa_graph_ptr &aut, unsigned threshold_states=0, unsigned threshold_cycles=0)
 Determinize a TBA using the powerset construction. More...
 
twa_graph_ptr tba_determinize_check (const twa_graph_ptr &aut, unsigned threshold_states=0, unsigned threshold_cycles=0, formula f=nullptr, const_twa_graph_ptr neg_aut=nullptr)
 Determinize a TBA and make sure it is correct. More...
 
twa_graph_ptr product (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, const output_aborter *aborter=nullptr)
 Intersect two automata using a synchronous product. More...
 
twa_graph_ptr product (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state, const output_aborter *aborter=nullptr)
 Intersect two automata using a synchronous product. More...
 
twa_graph_ptr product_or (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
 Sum two automata using a synchronous product. More...
 
twa_graph_ptr product_or (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state)
 Sum two automata using a synchronous product. More...
 
twa_graph_ptr product_xor (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
 XOR two deterministic automata using a synchronous product. More...
 
twa_graph_ptr product_xnor (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
 XNOR two automata using a synchronous product. More...
 
twa_graph_ptr product_susp (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right_susp)
 Build the product of an automaton with a suspendable automaton. More...
 
twa_graph_ptr product_or_susp (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right_susp)
 Build the "or" product of an automaton with a suspendable automaton. More...
 
twa_graph_ptr random_graph (int n, float d, const atomic_prop_set *ap, const bdd_dict_ptr &dict, unsigned n_accs=0, float a=0.1, float t=0.5, bool deterministic=false, bool state_acc=false, bool colored=false)
 Construct a twa randomly. More...
 
acc_cond::acc_code random_acceptance (unsigned n_accs)
 Build a random acceptance where each acceptance sets is used once. More...
 
void randomize (twa_graph_ptr &aut, bool randomize_states=true, bool randomize_edges=true)
 Randomize a TGBA. More...
 
void relabel_here (twa_graph_ptr &aut, relabeling_map *relmap)
 replace atomic propositions in an automaton More...
 
bool rabin_is_buchi_realizable (const const_twa_graph_ptr &aut)
 Check if aut is Rablin-like and Büchi-realizable. More...
 
twa_graph_ptr rabin_to_buchi_if_realizable (const const_twa_graph_ptr &aut)
 Convert a Rabin-like automaton into a Büchi automaton only when it can be done without changing the automaton structure. More...
 
twa_graph_ptr rabin_to_buchi_maybe (const const_twa_graph_ptr &aut)
 Convert a Rabin-like automaton into a Büchi automaton, preserving determinism when possible. More...
 
twa_graph_ptr remove_fin (const const_twa_graph_ptr &aut)
 Rewrite an automaton without Fin or f acceptance. More...
 
twa_graph_ptr to_finite (const_twa_graph_ptr aut, const char *alive="alive")
 Interpret the "live" part of an automaton as finite automaton. More...
 
twa_graph_ptr sbacc (twa_graph_ptr aut)
 Transform an automaton to use state-based acceptance. More...
 
twa_graph_ptr scc_filter (const const_twa_graph_ptr &aut, bool remove_all_useless=false, scc_info *given_si=nullptr)
 Prune unaccepting SCCs and remove superfluous acceptance conditions. More...
 
twa_graph_ptr scc_filter_states (const const_twa_graph_ptr &aut, bool remove_all_useless=false, scc_info *given_si=nullptr)
 Prune unaccepting SCCs. More...
 
twa_graph_ptr scc_filter_susp (const const_twa_graph_ptr &aut, bool remove_all_useless, bdd suspvars, bdd ignoredvars, bool early_susp, scc_info *given_si=nullptr)
 Prune unaccepting SCCs, superfluous acceptance sets, and suspension variables. More...
 
bool operator! (scc_info_options me)
 
scc_info_options operator& (scc_info_options left, scc_info_options right)
 
scc_info_options operator| (scc_info_options left, scc_info_options right)
 
std::ostream & dump_scc_info_dot (std::ostream &out, const_twa_graph_ptr aut, scc_info *sccinfo=nullptr)
 Dump the SCC graph of aut on out. More...
 
emptiness_check_ptr explicit_se05_search (const const_twa_ptr &a, option_map o=option_map())
 Returns an emptiness check on the spot::tgba automaton a. More...
 
emptiness_check_ptr bit_state_hashing_se05_search (const const_twa_ptr &a, size_t size, option_map o=option_map())
 Returns an emptiness checker on the spot::tgba automaton a. More...
 
emptiness_check_ptr se05 (const const_twa_ptr &a, option_map o)
 Wrapper for the two se05 implementations. More...
 
bool has_separate_sets (const const_twa_graph_ptr &aut)
 Whether the Inf and Fin numbers are disjoints. More...
 
twa_graph_ptr separate_sets_here (const twa_graph_ptr &aut)
 Separate the Fin and Inf sets used by an automaton. More...
 
twa_graph_ptr simulation (const const_twa_graph_ptr &automaton, int trans_pruning=-1)
 Attempt to reduce the automaton by direct simulation. More...
 
twa_graph_ptr simulation (const const_twa_graph_ptr &automaton, std::vector< bdd > *implications, int trans_pruning=-1)
 
twa_graph_ptr simulation_sba (const const_twa_graph_ptr &automaton, int trans_pruning=-1)
 
twa_graph_ptr split_edges (const const_twa_graph_ptr &aut)
 transform edges into transitions More...
 
twa_statistics stats_reachable (const const_twa_ptr &g)
 Compute statistics for an automaton. More...
 
twa_sub_statistics sub_stats_reachable (const const_twa_ptr &g)
 Compute sub statistics for an automaton. More...
 
unsigned long long count_all_transitions (const const_twa_graph_ptr &g)
 Count all transtitions, even unreachable ones. More...
 
bool is_terminal_automaton (const const_twa_graph_ptr &aut, scc_info *sm=nullptr, bool ignore_trivial_scc=false)
 Check whether an automaton is terminal. More...
 
bool is_weak_automaton (const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
 Check whether an automaton is weak. More...
 
bool is_very_weak_automaton (const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
 Check whether an automaton is very-weak. More...
 
bool is_inherently_weak_automaton (const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
 Check whether an automaton is inherently weak. More...
 
bool is_safety_automaton (const const_twa_graph_ptr &aut, scc_info *sm=nullptr)
 Check whether an automaton is a safety automaton. More...
 
bool is_liveness_automaton (const const_twa_graph_ptr &aut)
 Whether the automaton represents a liveness property. More...
 
void check_strength (const twa_graph_ptr &aut, scc_info *sm=nullptr)
 Check whether an automaton is weak or terminal. More...
 
twa_graph_ptr decompose_scc (const const_twa_graph_ptr &aut, const char *keep)
 Extract a sub-automaton of a given strength. More...
 
twa_graph_ptr decompose_scc (scc_info &sm, const char *keep)
 Extract a sub-automaton of a given strength. More...
 
twa_graph_ptr decompose_strength (const const_twa_graph_ptr &aut, const char *keep)
 
twa_graph_ptr decompose_scc (scc_info &sm, unsigned scc_num, bool accepting=false)
 Extract a sub-automaton above an SCC. More...
 
void strip_acceptance_here (twa_graph_ptr a)
 Remove all acceptance sets from a twa_graph. More...
 
twa_graph_ptr sl (const_twa_graph_ptr aut)
 Close the automaton by allowing letters to be duplicated. More...
 
bool is_stutter_invariant (formula f, twa_graph_ptr aut_f=nullptr)
 Check if a formula is stutter invariant. More...
 
bool is_stutter_invariant (twa_graph_ptr aut_f, const_twa_graph_ptr aut_nf=nullptr, int algo=0)
 Check if an automaton has the stutter invariance property. More...
 
trival check_stutter_invariance (twa_graph_ptr aut_f, formula f=nullptr, bool do_not_determinize=false, bool find_counterexamples=false)
 Check whether aut is stutter-invariant. More...
 
int is_stutter_invariant_forward_closed (twa_graph_ptr aut, const std::vector< bool > &sistates)
 Test if the set of stutter-invariant states is forward-closed. More...
 
std::vector< bool > make_stutter_invariant_forward_closed_inplace (twa_graph_ptr aut, const std::vector< bool > &sistates)
 Change the automaton so its set of stutter-invariant state is forward-closed. More...
 
twa_graph_ptr sum (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
 Sum two twa into a new twa, performing the union of the two input automata. More...
 
twa_graph_ptr sum (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state)
 Sum two twa into a new twa, performing the union of the two input automata. More...
 
twa_graph_ptr sum_and (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right)
 Sum two twa into a new twa, using a universal initial transition, performing the intersection of the two languages of the input automata. More...
 
twa_graph_ptr sum_and (const const_twa_graph_ptr &left, const const_twa_graph_ptr &right, unsigned left_state, unsigned right_state)
 Sum two twa into a new twa, using a universal initial transition, performing the intersection of the two languages of the input automata. More...
 
twa_graph_ptr split_2step (const const_twa_graph_ptr &aut, const bdd &output_bdd, bool complete_env=true)
 make each transition a 2-step transition, transforming the graph into an alternating arena More...
 
twa_graph_ptr split_2step (const const_twa_graph_ptr &aut, bool complete_env=true)
 Like split_2step but relying on the named property 'synthesis-outputs'. More...
 
twa_graph_ptr unsplit_2step (const const_twa_graph_ptr &aut)
 the inverse of split_2step More...
 
std::ostream & operator<< (std::ostream &os, synthesis_info::algo s)
 Stream algo. More...
 
std::ostream & operator<< (std::ostream &os, const synthesis_info &gi)
 Stream benchmarks and options. More...
 
mealy_like try_create_direct_strategy (formula f, const std::vector< std::string > &output_aps, synthesis_info &gi, bool want_strategy=false)
 Creates a strategy for the formula given by calling all intermediate steps. More...
 
bool solve_game (twa_graph_ptr arena, synthesis_info &gi)
 Solve a game, and update synthesis_info. More...
 
emptiness_check_ptr explicit_tau03_search (const const_twa_ptr &a, option_map o=option_map())
 Returns an emptiness checker on the spot::tgba automaton a. More...
 
emptiness_check_ptr explicit_tau03_opt_search (const const_twa_ptr &a, option_map o=option_map())
 Returns an emptiness checker on the spot::tgba automaton a. More...
 
twa_graph_ptr to_parity (const const_twa_graph_ptr &aut, const to_parity_options options=to_parity_options())
 Take an automaton with any acceptance condition and return an equivalent parity automaton. More...
 
twa_graph_ptr to_parity_old (const const_twa_graph_ptr &aut, bool pretty_print=false)
 Take an automaton with any acceptance condition and return an equivalent parity automaton. More...
 
 SPOT_DEPRECATED ("use to_parity() instead") twa_graph_ptr iar(const const_twa_graph_ptr &aut
 Turn a Rabin-like or Streett-like automaton into a parity automaton based on the index appearence record (IAR) More...
 
 SPOT_DEPRECATED ("use to_parity() and spot::acc_cond::is_rabin_like() instead") twa_graph_ptr iar_maybe(const const_twa_graph_ptr &aut
 Turn a Rabin-like or Streett-like automaton into a parity automaton based on the index appearence record (IAR) More...
 
twa_graph_ptr parity_type_to_parity (const twa_graph_ptr &aut)
 Convert an automaton into a parity max automaton preserving structure when possible. More...
 
twa_graph_ptr buchi_type_to_buchi (const twa_graph_ptr &aut)
 Convert an automaton into a Büchi automaton preserving structure when possible. More...
 
twa_graph_ptr co_buchi_type_to_co_buchi (const twa_graph_ptr &aut)
 Convert an automaton into a co-Büchi automaton preserving structure when possible. More...
 
twa_graph_ptr to_generalized_buchi (const const_twa_graph_ptr &aut)
 Take an automaton with any acceptance condition and return an equivalent Generalized Büchi automaton. More...
 
twa_graph_ptr streett_to_generalized_buchi (const const_twa_graph_ptr &in)
 Convert Streett acceptance into generalized Büchi acceptance. More...
 
twa_graph_ptr streett_to_generalized_buchi_maybe (const const_twa_graph_ptr &in)
 Convert Streett acceptance into generalized Büchi. More...
 
twa_graph_ptr to_generalized_rabin (const const_twa_graph_ptr &aut, bool share_inf=false)
 Take an automaton with any acceptance condition and return an equivalent Generalized Rabin automaton. More...
 
twa_graph_ptr to_generalized_streett (const const_twa_graph_ptr &aut, bool share_fin=false)
 Take an automaton with any acceptance condition and return an equivalent Generalized Streett automaton. More...
 
twa_graph_ptr dnf_to_streett (const const_twa_graph_ptr &aut, bool original_states=false)
 Converts any DNF acceptance condition into Streett-like. More...
 
twa_graph_ptr to_weak_alternating (const_twa_graph_ptr &aut, bool less=false)
 Convert an alternating automaton to a weak alternating automaton. More...
 
twa_word_ptr make_twa_word (const bdd_dict_ptr &dict)
 Create an empty twa_word. More...
 
twa_word_ptr make_twa_word (const twa_run_ptr &run)
 Create a twa_word from a twa_run. More...
 
twa_word_ptr parse_word (const std::string &word, const bdd_dict_ptr &dict)
 Parse a twa_word. More...
 
bool operator! (zielonka_tree_options me)
 
zielonka_tree_options operator& (zielonka_tree_options left, zielonka_tree_options right)
 
zielonka_tree_options operator| (zielonka_tree_options left, zielonka_tree_options right)
 
zielonka_tree_options operator- (zielonka_tree_options left, zielonka_tree_options right)
 
twa_graph_ptr zielonka_tree_transform (const const_twa_graph_ptr &aut)
 Paritize an automaton using Zielonka tree. More...
 
bool operator! (acd_options me)
 
acd_options operator& (acd_options left, acd_options right)
 
acd_options operator| (acd_options left, acd_options right)
 
acd_options operator- (acd_options left, acd_options right)
 
twacube_ptr make_twacube (const std::vector< std::string > aps)
 
spot::cube satone_to_cube (bdd one, cubeset &cubeset, std::unordered_map< int, int > &binder)
 Transform one truth assignment represented as a BDD into a cube cube passed in parameter. The parameter binder map bdd indexes to cube indexes. More...
 
bdd cube_to_bdd (spot::cube cube, const cubeset &cubeset, std::unordered_map< int, int > &reverse_binder)
 Transform a cube cube into bdd using the map that bind cube indexes to bdd indexes. More...
 
std::vector< std::string > * extract_aps (spot::const_twa_graph_ptr aut, std::unordered_map< int, int > &ap_binder)
 Extract the atomic propositions from the automaton. This method also fill the binder, i.e. the mapping between BDD indexes to cube indexes. More...
 
twacube_ptr twa_to_twacube (spot::const_twa_graph_ptr aut)
 Convert a twa into a twacube. More...
 
spot::twa_graph_ptr twacube_to_twa (spot::twacube_ptr twacube, spot::bdd_dict_ptr d=nullptr)
 Convert a twacube into a twa. When \d is specified, the BDD_dict in parameter is used rather than creating a new one. More...
 
bool are_equivalent (const spot::twacube_ptr twacube, const spot::const_twa_graph_ptr twa)
 Check wether a twacube and a twa are equivalent. More...
 
bool is_bare_word (const char *str)
 Whether a word is bare. More...
 
std::string quote_unless_bare_word (const std::string &str)
 Double-quote words that are not bare. More...
 
bool is_spin_ap (const char *str)
 Whether a word can be used as an atomic proposition for Spin 5. More...
 
bitvectmake_bitvect (size_t bitcount)
 Allocate a bit-vector of bitcount bits. More...
 
bitvect_arraymake_bitvect_array (size_t bitcount, size_t vectcount)
 Allocate vectcount bit-vectors of bitcount bits. More...
 
std::ostream & escape_rfc4180 (std::ostream &os, const std::string &str)
 Double characters " in strings. More...
 
std::ostream & escape_latex (std::ostream &os, const std::string &str)
 Escape special LaTeX characters. More...
 
std::ostream & escape_html (std::ostream &os, const std::string &str)
 Escape special HTML characters. More...
 
std::ostream & escape_str (std::ostream &os, const std::string &str)
 Escape characters ", \, and \n in str. More...
 
std::string escape_str (const std::string &str)
 Escape characters ", \, and \n in str. More...
 
std::ostream & quote_shell_string (std::ostream &os, const char *str)
 Output str between simple quote or double quotes. More...
 
size_t wang32_hash (size_t key)
 Thomas Wang's 32 bit hash function. More...
 
size_t knuth32_hash (size_t key)
 Knuth's Multiplicative hash function. More...
 
template<class It >
size_t fnv_hash (It begin, It end)
 Fowler-Noll-Vo hash function. More...
 
void int_array_array_compress2 (const int *array, size_t n, int *dest, size_t &dest_size)
 Compress an int array of size n into a int array. More...
 
void int_array_array_decompress2 (const int *array, size_t array_size, int *res, size_t size)
 Uncompress an int array of size array_size into a int array of size size. More...
 
void int_vector_vector_compress (const std::vector< int > &input, std::vector< unsigned int > &output)
 Compress an int vector into a vector of unsigned int. More...
 
void int_vector_vector_decompress (const std::vector< unsigned int > &array, std::vector< int > &output, size_t size)
 Uncompress a vector of unsigned int into a vector of size size. More...
 
const std::vector< unsigned int > * int_array_vector_compress (const int *array, size_t n)
 Compress an int array if size n into a vector of unsigned int. More...
 
void int_vector_array_decompress (const std::vector< unsigned int > *array, int *res, size_t size)
 Uncompress a vector of unsigned int into an int array of size size. More...
 
void int_array_array_compress (const int *array, size_t n, int *dest, size_t &dest_size)
 Compress an int array of size n into a int array. More...
 
void int_array_array_decompress (const int *array, size_t array_size, int *res, size_t size)
 Uncompress an int array of size array_size into a int array of size size. More...
 
void srand (unsigned int seed)
 Reset the seed of the pseudo-random number generator. More...
 
int rrand (int min, int max)
 Compute a pseudo-random integer value between min and max included. More...
 
int mrand (int max)
 Compute a pseudo-random integer value between 0 and max-1 included. More...
 
double drand ()
 Compute a pseudo-random double value between 0.0 and 1.0 (1.0 excluded). More...
 
double nrand ()
 Compute a pseudo-random double value following a standard normal distribution. (Odeh & Evans) More...
 
template<class iterator_type >
void mrandom_shuffle (iterator_type &&first, iterator_type &&last)
 Shuffle the container using mrand function above. This allows to get rid off shuffle or random_shuffle that use uniform_distribution and RandomIterator that are not portables. More...
 
temporary_filecreate_tmpfile (const char *prefix, const char *suffix=nullptr)
 Create a temporary file. More...
 
open_temporary_filecreate_open_tmpfile (const char *prefix, const char *suffix=nullptr)
 Create a temporary file and leave it open for writing. More...
 
void cleanup_tmpfiles ()
 Delete all temporary files. More...
 
constexpr bool operator== (trival a, trival b)
 
constexpr bool operator!= (trival a, trival b)
 
constexpr trival operator&& (trival a, trival b)
 
constexpr trival operator&& (bool a, trival b)
 
constexpr trival operator&& (trival a, bool b)
 
constexpr trival operator|| (trival a, trival b)
 
constexpr trival operator|| (bool a, trival b)
 
constexpr trival operator|| (trival a, bool b)
 
std::ostream & operator<< (std::ostream &os, trival v)
 
std::ostream & operator<< (std::ostream &os, const acc_cond &acc)
 
bdd formula_to_bdd (formula f, const bdd_dict_ptr &d, void *for_me)
 Convert a Boolean formula into a BDD. More...
 
template<typename T >
bdd formula_to_bdd (formula f, const bdd_dict_ptr &d, const std::shared_ptr< T > &for_me)
 Convert a Boolean formula into a BDD. More...
 
aig_ptr mealy_machine_to_aig (const const_twa_graph_ptr &m, const char *mode)
 Convert a mealy (like) machine into an aig relying on the transformation described by mode. More...
 
aig_ptr mealy_machine_to_aig (const twa_graph_ptr &m, const char *mode, const std::vector< std::string > &ins, const std::vector< std::string > &outs)
 Convert a mealy (like) machine into an aig relying on the transformation described by mode. More...
 
aig_ptr mealy_machine_to_aig (const mealy_like &m, const char *mode)
 Convert a mealy (like) machine into an aig relying on the transformation described by mode. More...
 
aig_ptr mealy_machine_to_aig (mealy_like &m, const char *mode, const std::vector< std::string > &ins, const std::vector< std::string > &outs)
 Convert a mealy (like) machine into an aig relying on the transformation described by mode. More...
 
aig_ptr mealy_machines_to_aig (const std::vector< const_twa_graph_ptr > &m_vec, const char *mode)
 Convert multiple mealy machines into an aig relying on the transformation described by mode. More...
 
aig_ptr mealy_machines_to_aig (const std::vector< mealy_like > &m_vec, const char *mode)
 Convert multiple mealy machines into an aig relying on the transformation described by mode. More...
 
aig_ptr mealy_machines_to_aig (const std::vector< const_twa_graph_ptr > &m_vec, const char *mode, const std::vector< std::string > &ins, const std::vector< std::vector< std::string >> &outs)
 Convert multiple mealy machines into an aig relying on the transformation described by mode. More...
 
aig_ptr mealy_machines_to_aig (const std::vector< mealy_like > &m_vec, const char *mode, const std::vector< std::string > &ins, const std::vector< std::vector< std::string >> &outs)
 Convert multiple mealy machines into an aig relying on the transformation described by mode. More...
 
twa_graph_ptr cleanup_acceptance_here (twa_graph_ptr aut, bool strip=true)
 Remove useless acceptance sets. More...
 
twa_graph_ptr cleanup_acceptance (const_twa_graph_ptr aut, bool strip=true)
 Remove useless acceptance sets. More...
 
twa_graph_ptr simplify_acceptance_here (twa_graph_ptr aut)
 Simplify an acceptance condition. More...
 
twa_graph_ptr simplify_acceptance (const_twa_graph_ptr aut)
 Simplify an acceptance condition. More...
 
bool contains (const_twa_graph_ptr left, const_twa_ptr right)
 Test if the language of right is included in that of left. More...
 
bool contains (const_twa_graph_ptr left, formula right)
 Test if the language of right is included in that of left. More...
 
bool contains (formula left, const_twa_ptr right)
 Test if the language of right is included in that of left. More...
 
bool contains (formula left, formula right)
 Test if the language of right is included in that of left. More...
 
bool are_equivalent (const_twa_graph_ptr left, const_twa_graph_ptr right)
 Test if the language of left is equivalent to that of right. More...
 
bool are_equivalent (const_twa_graph_ptr left, formula right)
 Test if the language of left is equivalent to that of right. More...
 
bool are_equivalent (formula left, const_twa_graph_ptr right)
 Test if the language of left is equivalent to that of right. More...
 
bool are_equivalent (formula left, formula right)
 Test if the language of left is equivalent to that of right. More...
 
twa_graph_ptr partial_degeneralize (const const_twa_graph_ptr &a, acc_cond::mark_t todegen)
 @} More...
 
twa_graph_ptr partial_degeneralize (twa_graph_ptr a)
 @} More...
 
std::vector< acc_cond::mark_tpropagate_marks_vector (const const_twa_graph_ptr &aut, const scc_info *si=nullptr)
 Propagate marks around the automaton. More...
 
void propagate_marks_here (twa_graph_ptr &aut, const scc_info *si=nullptr)
 Propagate marks around the automaton. More...
 
std::ostream & print_pg (std::ostream &os, const const_twa_graph_ptr &arena)
 Print a parity game using PG-solver syntax. More...
 
void pg_print (std::ostream &os, const const_twa_graph_ptr &arena)
 Print a parity game using PG-solver syntax. More...
 
void set_state_players (twa_graph_ptr arena, const region_t &owners)
 Set the owner for all the states. More...
 
void set_state_players (twa_graph_ptr arena, region_t &&owners)
 Set the owner for all the states. More...
 
const strategy_t & get_strategy (const_twa_graph_ptr arena)
 Get or set the strategy. More...
 
void set_strategy (twa_graph_ptr arena, const strategy_t &strat)
 Get or set the strategy. More...
 
void set_strategy (twa_graph_ptr arena, strategy_t &&strat)
 Get or set the strategy. More...
 
void set_state_winners (twa_graph_ptr arena, const region_t &winners)
 Set the winner for all the states. More...
 
void set_state_winners (twa_graph_ptr arena, region_t &&winners)
 Set the winner for all the states. More...
 
twa_graph_ptr split_separated_mealy (const const_twa_graph_ptr &m)
 split a separated mealy machine More...
 
void split_separated_mealy_here (const twa_graph_ptr &m)
 split a separated mealy machine More...
 
twa_graph_ptr reduce_mealy (const const_twa_graph_ptr &mm, bool output_assignment=true)
 reduce an (in)completely specified mealy machine More...
 
void reduce_mealy_here (twa_graph_ptr &mm, bool output_assignment=true)
 reduce an (in)completely specified mealy machine More...
 
void simplify_mealy_here (twa_graph_ptr &m, int minimize_lvl, bool split_out)
 Convenience function to call minimize_mealy or reduce_mealy. Uses the same convention as ltlsynt for minimize_lvl (or the field minimize_lvl of si): More...
 
void simplify_mealy_here (twa_graph_ptr &m, synthesis_info &si, bool split_out)
 Convenience function to call minimize_mealy or reduce_mealy. Uses the same convention as ltlsynt for minimize_lvl (or the field minimize_lvl of si): More...
 
twa_graph_ptr cleanup_parity (const const_twa_graph_ptr &aut, bool keep_style=false)
 Remove useless acceptance sets of an automaton with parity acceptance. More...
 
twa_graph_ptr cleanup_parity_here (twa_graph_ptr aut, bool keep_style=false)
 Remove useless acceptance sets of an automaton with parity acceptance. More...
 
twa_graph_ptr colorize_parity (const const_twa_graph_ptr &aut, bool keep_style=false)
 Colorize an automaton with parity acceptance. More...
 
twa_graph_ptr colorize_parity_here (twa_graph_ptr aut, bool keep_style=false)
 Colorize an automaton with parity acceptance. More...
 
twa_graph_ptr reduce_parity (const const_twa_graph_ptr &aut, bool colored=false, bool layered=false)
 Reduce the parity acceptance condition to use a minimal number of colors. More...
 
twa_graph_ptr reduce_parity_here (twa_graph_ptr aut, bool colored=false, bool layered=false)
 Reduce the parity acceptance condition to use a minimal number of colors. More...
 
twa_graph_ptr cosimulation (const const_twa_graph_ptr &automaton, int trans_pruning=-1)
 Attempt to reduce the automaton by reverse simulation. More...
 
twa_graph_ptr cosimulation_sba (const const_twa_graph_ptr &automaton, int trans_pruning=-1)
 Attempt to reduce the automaton by reverse simulation. More...
 
twa_graph_ptr iterated_simulations (const const_twa_graph_ptr &automaton, int trans_pruning=-1)
 Iterate simulation() and cosimulation(). More...
 
twa_graph_ptr iterated_simulations_sba (const const_twa_graph_ptr &automaton, int trans_pruning=-1)
 Iterate simulation() and cosimulation(). More...
 
twa_graph_ptr reduce_direct_sim (const const_twa_graph_ptr &aut)
 Attempt to reduce the automaton by direct simulation. More...
 
twa_graph_ptr reduce_direct_sim_sba (const const_twa_graph_ptr &aut)
 Attempt to reduce the automaton by direct simulation. More...
 
twa_graph_ptr reduce_direct_cosim (const const_twa_graph_ptr &aut)
 Attempt to reduce the automaton by reverse simulation. More...
 
twa_graph_ptr reduce_direct_cosim_sba (const const_twa_graph_ptr &aut)
 Attempt to reduce the automaton by reverse simulation. More...
 
twa_graph_ptr reduce_iterated (const const_twa_graph_ptr &aut)
 Iterate reduce_direct_sim() and reduce_direct_cosim(). More...
 
twa_graph_ptr reduce_iterated_sba (const const_twa_graph_ptr &aut)
 Iterate reduce_direct_sim() and reduce_direct_cosim(). More...
 
twa_graph_ptr sl2_inplace (twa_graph_ptr aut)
 Close the automaton by allowing letters to be duplicated. More...
 
twa_graph_ptr sl2 (const_twa_graph_ptr aut)
 Close the automaton by allowing letters to be duplicated. More...
 
twa_graph_ptr closure_inplace (twa_graph_ptr aut)
 Close the automaton by allowing duplicate letter removal. More...
 
twa_graph_ptr closure (const_twa_graph_ptr aut)
 Close the automaton by allowing duplicate letter removal. More...
 
std::vector< bool > stutter_invariant_states (const_twa_graph_ptr pos, const_twa_graph_ptr neg=nullptr)
 Determinate the states that are stutter-invariant in pos. More...
 
std::vector< bool > stutter_invariant_states (const_twa_graph_ptr pos, formula f_pos)
 Determinate the states that are stutter-invariant in pos. More...
 
void highlight_stutter_invariant_states (twa_graph_ptr pos, formula f_pos, unsigned color=0)
 Highlight the states of pos that are stutter-invariant. More...
 
void highlight_stutter_invariant_states (twa_graph_ptr pos, const_twa_graph_ptr neg=nullptr, unsigned color=0)
 Highlight the states of pos that are stutter-invariant. More...
 
std::vector< bdd > stutter_invariant_letters (const_twa_graph_ptr pos, const_twa_graph_ptr neg=nullptr)
 Determinate the letters with which each state is stutter-invariant. More...
 
std::vector< bdd > stutter_invariant_letters (const_twa_graph_ptr pos, formula f_pos)
 Determinate the letters with which each state is stutter-invariant. More...
 
twa_graph_ptr ltl_to_game (const formula &f, const std::vector< std::string > &all_outs, synthesis_info &gi)
 Creates a game from a specification and a set of output propositions. More...
 
twa_graph_ptr ltl_to_game (const formula &f, const std::vector< std::string > &all_outs)
 Creates a game from a specification and a set of output propositions. More...
 
twa_graph_ptr ltl_to_game (const std::string &f, const std::vector< std::string > &all_outs, synthesis_info &gi)
 Creates a game from a specification and a set of output propositions. More...
 
twa_graph_ptr ltl_to_game (const std::string &f, const std::vector< std::string > &all_outs)
 Creates a game from a specification and a set of output propositions. More...
 
twa_graph_ptr solved_game_to_mealy (twa_graph_ptr arena, synthesis_info &gi)
 creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More...
 
twa_graph_ptr solved_game_to_mealy (twa_graph_ptr arena)
 creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More...
 
twa_graph_ptr solved_game_to_separated_mealy (twa_graph_ptr arena, synthesis_info &gi)
 creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More...
 
twa_graph_ptr solved_game_to_separated_mealy (twa_graph_ptr arena)
 creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More...
 
twa_graph_ptr solved_game_to_split_mealy (twa_graph_ptr arena, synthesis_info &gi)
 creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More...
 
twa_graph_ptr solved_game_to_split_mealy (twa_graph_ptr arena)
 creates a mealy machine from a solved game arena taking into account the options given in gi. This concerns in particular whether or not the machine is to be reduced and how. solved_game_to_mealy can return any type of mealy machine. In fact it will return the type that necessitates no additional operations More...
 
std::pair< std::vector< formula >, std::vector< std::set< formula > > > split_independant_formulas (formula f, const std::vector< std::string > &outs)
 Seeks to decompose a formula into independently synthesizable sub-parts. The conjunction of all sub-parts then satisfies the specification. More...
 
std::pair< std::vector< formula >, std::vector< std::set< formula > > > split_independant_formulas (const std::string &f, const std::vector< std::string > &outs)
 Seeks to decompose a formula into independently synthesizable sub-parts. The conjunction of all sub-parts then satisfies the specification. More...
 
twa_graph_ptr acd_transform (const const_twa_graph_ptr &aut, bool colored=false)
 Paritize an automaton using ACD. More...
 
twa_graph_ptr acd_transform_sbacc (const const_twa_graph_ptr &aut, bool colored=false, bool order_heuristic=true)
 Paritize an automaton using ACD. More...
 

Variables

constexpr const char * default_unabbrev_string = "eFGiMW^"
 
bool pretty_print = false)
 
enum  parity_kind { parity_kind_max , parity_kind_min , parity_kind_same , parity_kind_any }
 Parity kind type. More...
 
enum  parity_style { parity_style_odd , parity_style_even , parity_style_same , parity_style_any }
 Parity style type. More...
 
twa_graph_ptr change_parity (const const_twa_graph_ptr &aut, parity_kind kind, parity_style style)
 Change the parity acceptance of an automaton. More...
 
twa_graph_ptr change_parity_here (twa_graph_ptr aut, parity_kind kind, parity_style style)
 Parity kind type. More...
 
enum class  edge_filter_choice { keep , ignore , cut }
 An edge_filter may be called on each edge to decide what to do with it. More...
 
typedef edge_filter_choice(* edge_filter) (const twa_graph::edge_storage_t &e, unsigned dst, void *filter_data)
 An edge_filter may be called on each edge to decide what to do with it. More...
 
typedef struct spot::process_timer process_timer
 Struct used to start and stop both timer and stopwatch clocks. More...
 
std::ostream & operator<< (std::ostream &os, const timer &dt)
 Struct used to start and stop both timer and stopwatch clocks. More...
 

Detailed Description

This file aggregates all classes and typedefs necessary to build a kripke that is thread safe

Typedef Documentation

◆ cspins_state

typedef int* spot::cspins_state

A Spins state is represented as an array of integer Note that this array has two reserved slots (position 0 an 1).

At position 0 we store the hash associated to the state to avoid multiple computations.

At position 1 we store the size of the state: keeping this information allows to compress the state

◆ cube

using spot::cube = typedef unsigned*

A cube is only a set of bits in memory.

This set can be seen as two bitsets

  • true_var : a bitset representing variables that are set to true
  • false_var : a bitset representing variables that are set to false

In the two vectors a bit set to 1 represent a variable set to true (resp. false) for the true_var (resp. false_var)

Warning : a variable cannot be set in both bitset at the same time (consistency! cannot be true and false)

The cube for (a & !b) will be repensented by :

  • true_var = 1 0
  • false_var = 0 1

To represent free variables such as in (a & !b) | (a & b) (wich is equivalent to (a) with b free)

  • true_var : 1 0
  • false_var : 0 0 This exemple shows that the representation of free variables is done by unsetting variable in both vector

To be memory efficient, these two bitsets are contigous in memory i.e. if we want to represent 35 variables, a cube will be represented by 4 unsigned int contiguous in memory. The 35 first bits represent truth values. The 29 bits following are useless. Then, the 35 bits represents false value and the rest is useless.

Note that useless bits are only to perform some action efficiently, i.e. only by ignoring them. The manipulation of cubes must be done using the cubeset class

◆ ltsmin_kripkecube_ptr

shortcut to manipulate the kripke below

◆ process_timer

Struct used to start and stop both timer and stopwatch clocks.

◆ product_states

typedef std::vector<std::pair<unsigned, unsigned> > spot::product_states

Automata constructed by product() contain a property named "product-states" with this type.

◆ shared_state_set

typedef std::unordered_set<shared_state, state_shared_ptr_hash, state_shared_ptr_equal> spot::shared_state_set

Unordered set of shared states.

◆ state_map

template<class val >
using spot::state_map = typedef std::unordered_map<const state*, val, state_ptr_hash, state_ptr_equal>

Unordered map of abstract states.

Destroying each state if needed is the user's responsibility.

◆ state_set

typedef std::unordered_set<const state*, state_ptr_hash, state_ptr_equal> spot::state_set

Unordered set of abstract states.

Destroying each state if needed is the user's responsibility.

See also
state_unicity_table

Enumeration Type Documentation

◆ mc_algorithm

enum spot::mc_algorithm
strong

The list of parallel model-checking algorithms available.

Enumerator
BLOEMEN_EC 

Bloemen.16.hvc emptiness check.

BLOEMEN_SCC 

Bloemen.16.ppopp SCC computation.

CNDFS 

Evangelista.12.atva emptiness check.

DEADLOCK 

Check wether there is a deadlock.

REACHABILITY 

Only perform a reachability algorithm.

SWARMING 

Holzmann.11.ieee applied to renault.13.lpar.

◆ mc_rvalue

enum spot::mc_rvalue
strong
Enumerator
DEADLOCK 

A deadlock has been found.

EMPTY 

The product is empty.

FAILURE 

The Algorithm finished abnormally.

NO_DEADLOCK 

No deadlock has been found.

NOT_EMPTY 

The product is not empty.

SUCCESS 

The Algorithm finished normally.

◆ ocheck

enum spot::ocheck
strong

Enum used to change the behavior of is_obligation().

◆ pool_type

enum spot::pool_type
strong

A enum class to define the policy of the fixed_sized_pool. We propose 2 policies for the pool:

  • Safe: ensure (when used with memcheck) that each allocation is deallocated one at a time
  • Unsafe: rely on the fact that deallocating the pool also release all elements it contains. This case is usefull in a multithreaded environnement with multiple fixed_sized_pool allocating the same ressource. In this case it's hard to detect wich pool has allocated some ressource.

Function Documentation

◆ are_equivalent()

bool spot::are_equivalent ( const spot::twacube_ptr  twacube,
const spot::const_twa_graph_ptr  twa 
)

Check wether a twacube and a twa are equivalent.

◆ atomic_prop_cmp()

int spot::atomic_prop_cmp ( const fnode f,
const fnode g 
)

Order two atomic propositions.

◆ bdd_format_accset()

std::string spot::bdd_format_accset ( const bdd_dict_ptr &  dict,
bdd  b 
)

Format a BDD as a set of acceptance conditions.

This is used when saving a TGBA.

Parameters
dictThe dictionary to use, to lookup variables.
bThe BDD to print.
Returns
The BDD formated as a string.

◆ bdd_format_formula()

std::string spot::bdd_format_formula ( const bdd_dict_ptr &  dict,
bdd  b 
)

Format a BDD as a formula.

Parameters
dictThe dictionary to use, to lookup variables.
bThe BDD to print.
Returns
The BDD formated as a string.

◆ bdd_format_isop()

std::string spot::bdd_format_isop ( const bdd_dict_ptr &  dict,
bdd  b 
)

Format a BDD as an irredundant sum of product.

Parameters
dictThe dictionary to use, to lookup variables.
bThe BDD to print.
Returns
The BDD formated as a string.

◆ bdd_format_sat()

std::string spot::bdd_format_sat ( const bdd_dict_ptr &  dict,
bdd  b 
)

Format a BDD as a list of literals.

This assumes that b is a conjunction of literals.

Parameters
dictThe dictionary to use, to lookup variables.
bThe BDD to print.
Returns
The BDD formated as a string.

◆ bdd_format_set()

std::string spot::bdd_format_set ( const bdd_dict_ptr &  dict,
bdd  b 
)

Format a BDD as a set.

Parameters
dictThe dictionary to use, to lookup variables.
bThe BDD to print.
Returns
The BDD formated as a string.

◆ bdd_print_accset()

std::ostream& spot::bdd_print_accset ( std::ostream &  os,
const bdd_dict_ptr &  dict,
bdd  b 
)

Print a BDD as a set of acceptance conditions.

This is used when saving a TGBA.

Parameters
osThe output stream.
dictThe dictionary to use, to lookup variables.
bThe BDD to print.
Returns
The BDD formated as a string.

◆ bdd_print_formula()

std::ostream& spot::bdd_print_formula ( std::ostream &  os,
const bdd_dict_ptr &  dict,
bdd  b 
)

Print a BDD as a formula.

Parameters
osThe output stream.
dictThe dictionary to use, to lookup variables.
bThe BDD to print.

◆ bdd_print_isop()

std::ostream& spot::bdd_print_isop ( std::ostream &  os,
const bdd_dict_ptr &  dict,
bdd  b 
)

Print a BDD as an irredundant sum of product.

Parameters
osThe output stream.
dictThe dictionary to use, to lookup variables.
bThe BDD to print.

◆ bdd_print_sat()

std::ostream& spot::bdd_print_sat ( std::ostream &  os,
const bdd_dict_ptr &  dict,
bdd  b 
)

Print a BDD as a list of literals.

This assumes that b is a conjunction of literals.

Parameters
osThe output stream.
dictThe dictionary to use, to lookup variables.
bThe BDD to print.

◆ bdd_print_set()

std::ostream& spot::bdd_print_set ( std::ostream &  os,
const bdd_dict_ptr &  dict,
bdd  b 
)

Print a BDD as a set.

Parameters
osThe output stream.
dictThe dictionary to use, to lookup variables.
bThe BDD to print.

◆ bdd_to_formula()

formula spot::bdd_to_formula ( bdd  f,
const bdd_dict_ptr  d 
)

Convert a BDD into a formula.

Format the BDD as an irredundant sum of product (see the minato_isop class for details) and map the BDD variables back into their atomic propositions. This works only for Boolean formulas, and all the BDD variables used in f should have been registered in d. Although the result has type formula, it obviously does not use any temporal operator.

◆ check_determinism()

void spot::check_determinism ( twa_graph_ptr  aut)

Set the deterministic and semi-deterministic properties appropriately.

◆ check_strength()

void spot::check_strength ( const twa_graph_ptr &  aut,
scc_info sm = nullptr 
)

Check whether an automaton is weak or terminal.

This sets the "inherently weak", "weak", "very-weak" and "terminal" properties as appropriate.

Parameters
autthe automaton to check
sman scc_info object for the automaton if available (it will be built otherwise).

◆ cleanup_parity()

twa_graph_ptr spot::cleanup_parity ( const const_twa_graph_ptr &  aut,
bool  keep_style = false 
)

Remove useless acceptance sets of an automaton with parity acceptance.

If two sets with the same parity are separated by unused sets, then these two sets are merged. The input must be an automaton with a parity acceptance, otherwise an invalid_argument exception is thrown.

Parameters
autthe input automaton
keep_stylewhether the style of the parity acc is kept.
Returns
the automaton without useless acceptance sets.

◆ cleanup_parity_here()

twa_graph_ptr spot::cleanup_parity_here ( twa_graph_ptr  aut,
bool  keep_style = false 
)

Remove useless acceptance sets of an automaton with parity acceptance.

If two sets with the same parity are separated by unused sets, then these two sets are merged. The input must be an automaton with a parity acceptance, otherwise an invalid_argument exception is thrown.

Parameters
autthe input automaton
keep_stylewhether the style of the parity acc is kept.
Returns
the automaton without useless acceptance sets.

◆ cleanup_tmpfiles()

void spot::cleanup_tmpfiles ( )

Delete all temporary files.

Delete all temporary files that have been created but haven't been deleted so far. The verb "delete" should be understood as both the C++ delete operator (all temporary_file and open_temporary_file instance are destroyed) and as the file system operation (the actual files are removed).

Even in programs where temporary_file instance are consciously destroyed when they are not needed, cleanup_tmpfiles() could still be useful in signal handlers, for instance to clean all temporary files upon SIGINT.

◆ colorize_parity()

twa_graph_ptr spot::colorize_parity ( const const_twa_graph_ptr &  aut,
bool  keep_style = false 
)

Colorize an automaton with parity acceptance.

An automaton is said colored iff all the transitions belong to exactly one acceptance set. The algorithm achieves that by removing superfluous acceptance marks. It may introduce a new set to mark the transitions with no acceptance sets and a second set may be introduced to keep the style. The input must be an automaton with a parity acceptance, otherwise an invalid_argument exception is thrown.

Parameters
autthe input automaton
keep_stylewhether the style of the parity acc is kept.
Returns
the colorized automaton

◆ colorize_parity_here()

twa_graph_ptr spot::colorize_parity_here ( twa_graph_ptr  aut,
bool  keep_style = false 
)

Colorize an automaton with parity acceptance.

An automaton is said colored iff all the transitions belong to exactly one acceptance set. The algorithm achieves that by removing superfluous acceptance marks. It may introduce a new set to mark the transitions with no acceptance sets and a second set may be introduced to keep the style. The input must be an automaton with a parity acceptance, otherwise an invalid_argument exception is thrown.

Parameters
autthe input automaton
keep_stylewhether the style of the parity acc is kept.
Returns
the colorized automaton

◆ complement()

twa_graph_ptr spot::complement ( const const_twa_graph_ptr &  aut,
const output_aborter aborter = nullptr 
)

Complement a TωA.

This employs different complementation strategies depending on the type of the automaton.

If the input is alternating, the output may be alternating and is simply the result of calling dualize().

If the input is not alternating, the output will not be alternating, but could have any acceptance condition.

  • deterministic inputs are passed to dualize()
  • very weak automata are also dualized, and then passed to remove_alternation() to obtain a TGBA
  • any other type of input is determized before complementation.

If an output_aborter is supplied, it is used to abort the construction of larger automata.

complement_semidet() is not yet used.

◆ complement_semidet()

twa_graph_ptr spot::complement_semidet ( const const_twa_graph_ptr &  aut,
bool  show_names = false 
)

Complement a semideterministic TωA.

The automaton aut should be semideterministic.

Uses the NCSB algorithm described by F. Blahoudek, et al. [4]

◆ complete()

twa_graph_ptr spot::complete ( const const_twa_ptr &  aut)

Clone a twa and complete it.

If the TωA is incomplete and has an acceptance condition that is a tautology, it will be changed into a Büchi automaton.

◆ complete_here()

void spot::complete_here ( twa_graph_ptr  aut)

Complete a twa_graph in place.

If the TωA is incomplete and has an acceptance condition that is a tautology, it will be changed into a Büchi automaton.

◆ compsusp()

twa_graph_ptr spot::compsusp ( formula  f,
const bdd_dict_ptr &  dict,
bool  no_wdba = false,
bool  no_simulation = false,
bool  early_susp = false,
bool  no_susp_product = false,
bool  wdba_smaller = false,
bool  oblig = false 
)

Compositional translation algorithm with resetable suspension.

Described in "Compositional Approach to Suspension and Other Improvements to LTL Translation", Tomáš Babiak, Thomas Badie, Alexandre Duret-Lutz, Mojmír Křetínský, Jan Strejček (SPIN'13).

If no_wdba or no_simulation is true, the corresponding operation is not performed on the skeleton automaton. If early_susp is true, then composition starts on the transition that enters the accepting SCC, not just in the SCC itself. If no_susp_product is true, then the composition is not performed and the skeleton automaton is returned for debugging. If wdba_smaller is true, then the WDBA-minimization of the skeleton is used only if it produces a smaller automaton.

Finally the oblig flag is a work in progress and should not be set to true.

This interface is subject to change, and clients aiming for long-term stability should better use the services of the spot::translator class instead.

◆ couvreur99_new_check()

emptiness_check_result_ptr spot::couvreur99_new_check ( const const_twa_ptr &  a)

A shortcut to run the optimized emptiness check directly.

This is the same as get_couvreur99_new(a, {})->check().

◆ create_open_tmpfile()

open_temporary_file* spot::create_open_tmpfile ( const char *  prefix,
const char *  suffix = nullptr 
)

Create a temporary file and leave it open for writing.

Same as create_tmpfile, be leave the file open for writing. The open_temporary_file::fd() method returns the file descriptor.

◆ create_tmpfile()

temporary_file* spot::create_tmpfile ( const char *  prefix,
const char *  suffix = nullptr 
)

Create a temporary file.

The file name will start with prefix, be followed by 6 randomish characters and will end in suffix. Usually suffix is used to set an extension (you should include the dot).

The temporary file is created and left empty. If you need to fill it, consider using create_open_tmpfile() instead.

◆ cube_to_bdd()

bdd spot::cube_to_bdd ( spot::cube  cube,
const cubeset cubeset,
std::unordered_map< int, int > &  reverse_binder 
)

Transform a cube cube into bdd using the map that bind cube indexes to bdd indexes.

◆ decompose_scc() [1/3]

twa_graph_ptr spot::decompose_scc ( const const_twa_graph_ptr &  aut,
const char *  keep 
)

Extract a sub-automaton of a given strength.

The string keep should be a non-empty combination of the following letters:

  • 'w': keep only inherently weak SCCs (i.e., SCCs in which all transitions belong to the same acceptance sets) that are not terminal.
  • 't': keep terminal SCCs (i.e., inherently weak SCCs that are complete)
  • 's': keep strong SCCs (i.e., SCCs that are not inherently weak). Additionally, the string may contain comma-separated numbers representing SCC number, optionally prefixed by 'a' to denote the Nth accepting SCC.

This algorithm returns a subautomaton that contains all SCCs of the requested strength (or given SCC numbers), plus any upstream SCC (but adjusted not to be accepting). The output may be null if no SCC match a given strength. An exception will be raised if an incorrect SCC number is supplied.

The definition are basically those used in the following paper, except that we extract the "inherently weak" part instead of the weak part because we can now test for inherent weakness efficiently enough (not enumerating all cycles as suggested in the paper). [45]

Parameters
autthe automaton to decompose
keepa string specifying the strengths/SCCs to keep

◆ decompose_scc() [2/3]

twa_graph_ptr spot::decompose_scc ( scc_info sm,
const char *  keep 
)

Extract a sub-automaton of a given strength.

This works exactly like decompose_scc(const const_twa_graph_ptr&, const char*) but takes an scc_info as first argument. This avoids wasting time to reconstruct that object if one is already available.

◆ decompose_scc() [3/3]

twa_graph_ptr spot::decompose_scc ( scc_info sm,
unsigned  scc_num,
bool  accepting = false 
)

Extract a sub-automaton above an SCC.

This algorithm returns a subautomaton that contains the requested SCC, plus any upstream SCC (but adjusted not to be accepting).

Parameters
smthe SCC info map of the automaton
scc_numthe index in the map of the SCC to keep
acceptingif true, scc_num is interpreted as the Nth accepting SCC instead of the Nth SCC

◆ dnf_to_dca()

twa_graph_ptr spot::dnf_to_dca ( const_twa_graph_ptr  aut,
bool  named_states = false 
)

Converts an aut. with acceptance in DNF to a det. co-Büchi aut.

This function calls first nra_to_nca() in order to retrieve som information and then runs a breakpoint construction. The algorithm is described in section 4 of [5] .

aut The automaton to convert. named_states name each state for easier debugging.

◆ dnf_to_nca()

twa_graph_ptr spot::dnf_to_nca ( const_twa_graph_ptr  aut,
bool  named_states = false,
vect_nca_info *  nca_info = nullptr 
)

Converts an aut. with acceptance in DNF to a nondet. co-Büchi aut.

This function converts the Rabin-like automaton into a Strett-like automaton and then calls nsa_to_nca() on it. It is described in section 3.2 of [5] .

aut The automaton to convert. named_states name each state for easier debugging. nca_info retrieve information about state visited infinitely often.

◆ dtba_sat_minimize()

twa_graph_ptr spot::dtba_sat_minimize ( const const_twa_graph_ptr &  a,
bool  state_based = false,
int  max_states = -1 
)

Attempt to minimize a deterministic TBA with a SAT solver.

This calls dtba_sat_synthetize() in a loop, with a decreasing number of states, and returns the last successfully built TBA.

If no smaller TBA exist, this returns a null pointer.

◆ dtba_sat_minimize_assume()

twa_graph_ptr spot::dtba_sat_minimize_assume ( const const_twa_graph_ptr &  a,
bool  state_based = false,
int  max_states = -1,
int  param = 6 
)

Attempt to minimize a deterministic TBA incrementally with a SAT solver.

This acts like dtba_sat_synthetize() and obtains a first minimized automaton. Then, it adds assumptions, such that each assumption removes a new state and implies the previous assumptions. A first resolution is attempted assuming the last assumption (thus involving all the previous ones). If the problem is SAT several stages have just been won and all this process is restarted. Otherwise, we know that the minimal automaton can be obtained with fewer assumption. This automaton is found dichotomously.

If no smaller TBA exist, this returns a null pointer.

◆ dtba_sat_minimize_dichotomy()

twa_graph_ptr spot::dtba_sat_minimize_dichotomy ( const const_twa_graph_ptr &  a,
bool  state_based = false,
bool  langmap = false,
int  max_states = -1 
)

Attempt to minimize a deterministic TBA with a SAT solver.

This calls dtba_sat_synthetize() in a loop, but attempting to find the minimum number of states using a binary search. If no smaller TBA exist, this returns a null pointer.

◆ dtba_sat_minimize_incr()

twa_graph_ptr spot::dtba_sat_minimize_incr ( const const_twa_graph_ptr &  a,
bool  state_based = false,
int  max_states = -1,
int  param = 2 
)

Attempt to minimize a det. TBA with a SAT solver.

This acts like dtba_sat_synthetize() and obtains a first minimized automaton. Then, incrementally, it encodes the deletion of one state and solves it as many time as param value. If param >= 0, this process is fully repeated until the minimal automaton is found. Otherwise, it continues to delete states one by one incrementally until the minimal automaton is found.

If no smaller TBA exist, this returns a null pointer.

◆ dtba_sat_synthetize()

twa_graph_ptr spot::dtba_sat_synthetize ( const const_twa_graph_ptr &  a,
int  target_state_number,
bool  state_based = false 
)

Attempt to synthetize an equivalent deterministic TBA with a SAT solver.

Parameters
athe input TGA. It should have only one acceptance set and be deterministic. I.e., it should be a deterministic TBA.
target_state_numberthe desired number of states wanted in the resulting automaton. The result may have less than target_state_number reachable states.
state_basedset to true to force all outgoing transitions of a state to share the same acceptance condition, effectively turning the TBA into a BA.

If no equivalent deterministic TBA with target_state_number states is found, this returns a null pointer.

◆ dtwa_complement()

twa_graph_ptr spot::dtwa_complement ( const const_twa_graph_ptr &  aut)

Complement a deterministic TωA.

The automaton aut should be deterministic. It will be completed if it isn't already. In these conditions, complementing the automaton can be done by just complementing the acceptance condition.

In particular, this implies that an input that use generalized Büchi will be output as generalized co-Büchi.

Functions like to_generalized_buchi() or remove_fin() are frequently called after dtwa_complement() to obtain an easier acceptance condition (maybe at the cost of losing determinism.)

This function was deprecated in spot 2.4. Call the function spot::dualize() instead, that is able to complement any input automaton, not only deterministic ones.

◆ dtwa_sat_minimize()

twa_graph_ptr spot::dtwa_sat_minimize ( const const_twa_graph_ptr &  a,
unsigned  target_acc_number,
const acc_cond::acc_code target_acc,
bool  state_based = false,
int  max_states = -1,
bool  colored = false 
)

Attempt to minimize a deterministic TωA with a SAT solver.

This calls dtwa_sat_synthetize() in a loop, with a decreasing number of states, and returns the last successfully built TGBA.

If no smaller TGBA exists, this returns a null pointer.

◆ dtwa_sat_minimize_assume()

twa_graph_ptr spot::dtwa_sat_minimize_assume ( const const_twa_graph_ptr &  a,
unsigned  target_acc_number,
const acc_cond::acc_code target_acc,
bool  state_based = false,
int  max_states = -1,
bool  colored = false,
int  param = 6 
)

Attempt to minimize a deterministic TωA with a SAT solver.

This acts like dtba_sat_synthetize() and obtains a first minimized automaton. Then, it adds assumptions, such that each assumption removes a new state and implies the previous assumptions. A first resolution is attempted assuming the last assumption (thus involving all the previous ones). If the problem is SAT several stages have just been won and all this process is restarted. Otherwise, it is known that the minimal automaton can be obtained with fewer assumption. This automaton is found dichotomously.

If no smaller TGBA exists, this returns a null pointer.

◆ dtwa_sat_minimize_dichotomy()

twa_graph_ptr spot::dtwa_sat_minimize_dichotomy ( const const_twa_graph_ptr &  a,
unsigned  target_acc_number,
const acc_cond::acc_code target_acc,
bool  state_based = false,
bool  langmap = false,
int  max_states = -1,
bool  colored = false 
)

Attempt to minimize a deterministic TωA with a SAT solver.

This calls dtwa_sat_synthetize() in a loop, but attempting to find the minimum number of states using a binary search. If no smaller TBA exist, this returns a null pointer.

◆ dtwa_sat_minimize_incr()

twa_graph_ptr spot::dtwa_sat_minimize_incr ( const const_twa_graph_ptr &  a,
unsigned  target_acc_number,
const acc_cond::acc_code target_acc,
bool  state_based = false,
int  max_states = -1,
bool  colored = false,
int  param = 2 
)

Attempt to minimize a deterministic TωA with a SAT solver.

It acts like dtwa_sat_synthetisze() and obtains a first minimized automaton. Then, incrementally, it encodes and solves the deletion of one state as many time as param value. If param >= 0, this process is fully repeated until the minimal automaton is found. Otherwise, it continues to delete states one by one incrementally until the minimal automaton is found.

If no smaller TGBA exists, this returns a null pointer.

◆ dtwa_sat_synthetize()

twa_graph_ptr spot::dtwa_sat_synthetize ( const const_twa_graph_ptr &  a,
unsigned  target_acc_number,
const acc_cond::acc_code target_acc,
int  target_state_number,
bool  state_based = false,
bool  colored = false 
)

Attempt to synthetize an equivalent deterministic TωA with a SAT solver.

Parameters
athe input TωA. It should be a deterministic TωA.
target_acc_numberis the number of acceptance sets wanted in the result.
target_accthe target acceptance condition
target_state_numberis the desired number of states in the result. The output may have less than target_state_number reachable states.
state_basedset to true to force all outgoing transitions of a state to share the same acceptance conditions.
coloredif true, force all transitions to belong to exactly one acceptance set.

This functions attempts to find a TωA with target_acc_number acceptance sets and target_state_number states that is equivalent to a. If no such TωA is found, a null pointer is returned.

◆ dump_scc_info_dot()

std::ostream& spot::dump_scc_info_dot ( std::ostream &  out,
const_twa_graph_ptr  aut,
scc_info sccinfo = nullptr 
)

Dump the SCC graph of aut on out.

If sccinfo is not given, it will be computed.

◆ enable_utf8()

void spot::enable_utf8 ( )

Enable UTF-8 output for bdd printers.

◆ extract_aps()

std::vector<std::string>* spot::extract_aps ( spot::const_twa_graph_ptr  aut,
std::unordered_map< int, int > &  ap_binder 
)

Extract the atomic propositions from the automaton. This method also fill the binder, i.e. the mapping between BDD indexes to cube indexes.

◆ formula_to_bdd() [1/2]

template<typename T >
bdd spot::formula_to_bdd ( formula  f,
const bdd_dict_ptr &  d,
const std::shared_ptr< T > &  for_me 
)

Convert a Boolean formula into a BDD.

Convert the Boolean formula f into a BDD, using existing variables from d, and registering new ones as necessary. for_me, the address of the user of these BDD variables will be passed to d when registering the variables.

If you only use the BDD representation temporarily, for instance passing it right away to bdd_to_formula(), you should not forget to unregister the variables that have been registered for for_me. See bdd_dict::unregister_all_my_variables().

References formula_to_bdd().

◆ formula_to_bdd() [2/2]

bdd spot::formula_to_bdd ( formula  f,
const bdd_dict_ptr &  d,
void *  for_me 
)

Convert a Boolean formula into a BDD.

Convert the Boolean formula f into a BDD, using existing variables from d, and registering new ones as necessary. for_me, the address of the user of these BDD variables will be passed to d when registering the variables.

If you only use the BDD representation temporarily, for instance passing it right away to bdd_to_formula(), you should not forget to unregister the variables that have been registered for for_me. See bdd_dict::unregister_all_my_variables().

Referenced by formula_to_bdd().

◆ get_couvreur99_new()

emptiness_check_ptr spot::get_couvreur99_new ( const const_twa_ptr &  a,
option_map  o 
)

A rewritten version of the Couvreur emptiness check.

It is optimized to run on explicit automata (avoiding the memory allocations of the virtual, abstract interface. It also has specializations for weak and terminal automata.

◆ get_couvreur99_new_abstract()

emptiness_check_ptr spot::get_couvreur99_new_abstract ( const const_twa_ptr &  a,
option_map  o 
)

Same as above, but always uses the abstract interface.

This function is provided to test the efficiency of specializing our algorithms for explicit automata. It uses the same optimizations for weak and terminal automata as the one above.

◆ get_states_set()

std::set<const state*> spot::get_states_set ( const const_ta_ptr &  t)

Compute states set for an automaton.

◆ get_synthesis_output_aps()

std::vector<std::string> spot::get_synthesis_output_aps ( const const_twa_graph_ptr &  arena)

Get the vector with the names of the output propositions.

◆ highlight_languages()

void spot::highlight_languages ( twa_graph_ptr &  aut)

Color state that recognize identical language.

State that recognize a unique language will not be colored.

◆ highlight_semidet_sccs()

void spot::highlight_semidet_sccs ( scc_info si,
unsigned  color 
)

Highlight the deterministic part of the automaton.

In the case of a semideterministic automaton, highlights the states reachable from any accepting SCC.

Parameters
sithe SCC information of the automaton to process
colorthe color to give to states reachable from accepting SCCs.

◆ is_complete()

bool spot::is_complete ( const const_twa_graph_ptr &  aut)

Return true iff aut is complete.

An automaton is complete if its translation relation is total, i.e., each state as a successor for any possible configuration.

◆ is_inherently_weak_automaton()

bool spot::is_inherently_weak_automaton ( const const_twa_graph_ptr &  aut,
scc_info sm = nullptr 
)

Check whether an automaton is inherently weak.

An automaton is inherently weak if in any given SCC, there are only accepting cycles, or only rejecting cycles.

Parameters
autthe automaton to check
sman scc_info object for the automaton if available (it will be built otherwise).

In addition to returning the result as a Boolean, this will set the prop_inherently_weak() property of the automaton as a side-effect, so further calls will return in constant-time.

◆ is_input_deterministic_mealy()

bool spot::is_input_deterministic_mealy ( const const_twa_graph_ptr &  m)

Checks whether a mealy machine is input deterministic.

A machine is input deterministic if none of the states has two outgoing transitions that can agree on a common assignment of the input propositions. In case the mealy machine is split, the previous condition is tested only on states owned by player 0 (the environment).

Parameters
mThe automaton to be verified
See also
is_mealy

◆ is_liveness()

bool spot::is_liveness ( formula  f)

Check whether a formula represents a liveness property.

A formula represents a liveness property if any finite prefix can be extended into a word accepted by the formula.

The test is done by conversion to automaton. If you already have an automaton, use spot::is_liveness_automaton() instead.

◆ is_liveness_automaton()

bool spot::is_liveness_automaton ( const const_twa_graph_ptr &  aut)

Whether the automaton represents a liveness property.

An automaton represents a liveness property if after forcing the acceptance condition to true, the resulting automaton accepts all words. In other words, there is no prefix that cannot be extended into an accepting word.

◆ is_partially_degeneralizable()

acc_cond::mark_t spot::is_partially_degeneralizable ( const const_twa_graph_ptr &  aut,
bool  allow_inf = true,
bool  allow_fin = true,
std::vector< acc_cond::mark_t forbid = {} 
)

Is the automaton partially degeneralizable?

Return a mark M={m₁, m₂, ..., mₙ} such that either Inf(m₁)&Inf(m₂)&...&Inf(mₙ) or Fin(m₁)|Fin(m₂)|...|Fin(mₙ) appears in the acceptance condition of aut.

If multiple such marks exist the smallest such mark is returned. (This is important in case of overlapping options. E.g., in the formula Inf(0)&Inf(1)&Inf(3) | (Inf(0)&Inf(1))&Fin(2) we have two possible degeneralizations options {0,1,3}, and {0,1}. Degeneralizing for {0,1,3} and then {0,1} could enlarge the automaton by a factor 6, while degeneralizing by {0,1} and then some {x,y} may enlarge the automaton only by a factor 4.)

Return an empty mark otherwise if the automaton is not partially degeneralizable.

The optional arguments allow_inf and allow_fin, can be set to false to disallow one type of match.

◆ is_safety_automaton()

bool spot::is_safety_automaton ( const const_twa_graph_ptr &  aut,
scc_info sm = nullptr 
)

Check whether an automaton is a safety automaton.

A safety automaton has only accepting SCCs (or trivial SCCs).

A minimized WDBA (as returned by a successful run of minimize_obligation()) represents safety property if it is a safety automaton.

Parameters
autthe automaton to check
sman scc_info object for the automaton if available (it will be built otherwise).

◆ is_semi_deterministic()

bool spot::is_semi_deterministic ( const const_twa_graph_ptr &  aut)

Return true iff aut is semi-deterministic.

An automaton is semi-deterministic if the sub-automaton reachable from any accepting SCC is deterministic.

◆ is_terminal_automaton()

bool spot::is_terminal_automaton ( const const_twa_graph_ptr &  aut,
scc_info sm = nullptr,
bool  ignore_trivial_scc = false 
)

Check whether an automaton is terminal.

An automaton is terminal if it is weak, all its accepting SCCs are complete, and no accepting transitions lead to a non-accepting SCC.

If ignore_trivial_scc is set, accepting transitions from trivial SCCs are ignored.

This property guarantees that a word is accepted if it has some prefix that reaches an accepting transition.

Parameters
autthe automaton to check
sman scc_info object for the automaton if available (it will be built otherwise).

In addition to returning the result as a Boolean, this will set the prop_terminal() property of the automaton as a side-effect, so further calls will return in constant-time.

◆ is_very_weak_automaton()

bool spot::is_very_weak_automaton ( const const_twa_graph_ptr &  aut,
scc_info sm = nullptr 
)

Check whether an automaton is very-weak.

An automaton is very-weak if in any given SCC, all transitions belong to the same acceptance sets, and the SCC has only one state.

Parameters
autthe automaton to check
sman scc_info object for the automaton if available (it will be built otherwise).

In addition to returning the result as a Boolean, this will set the prop_very_weak() and prop_weak() properties of the automaton as a side-effect, so further calls will return in constant-time.

◆ is_weak_automaton()

bool spot::is_weak_automaton ( const const_twa_graph_ptr &  aut,
scc_info sm = nullptr 
)

Check whether an automaton is weak.

An automaton is weak if in any given SCC, all transitions belong to the same acceptance sets.

Parameters
autthe automaton to check
sman scc_info object for the automaton if available (it will be built otherwise).

In addition to returning the result as a Boolean, this will set the prop_weak() property of the automaton as a side-effect, so further calls will return in constant-time.

◆ language_map()

std::vector<unsigned> spot::language_map ( const const_twa_graph_ptr &  aut)

Identify states that recognize the same language.

The returned vector is the same size as the automaton's number of state. The number of different values (ignoring occurences) in the vector is the total number of recognized languages, states recognizing the same language have the same value.

The given automaton must be deterministic.

◆ list_formula_props()

std::list<std::string> spot::list_formula_props ( const formula f)

List the properties of formula f.

◆ make_bitvect()

bitvect* spot::make_bitvect ( size_t  bitcount)

Allocate a bit-vector of bitcount bits.

The resulting object should be released with delete.

◆ make_bitvect_array()

bitvect_array* spot::make_bitvect_array ( size_t  bitcount,
size_t  vectcount 
)

Allocate vectcount bit-vectors of bitcount bits.

The resulting bitvect_array should be released with delete.

◆ make_twa_word() [1/2]

twa_word_ptr spot::make_twa_word ( const bdd_dict_ptr &  dict)
inline

Create an empty twa_word.

Note that empty twa_word are invalid and cannot be printed. After creating an empty twa_word, you should at least populate the cycle.

◆ make_twa_word() [2/2]

twa_word_ptr spot::make_twa_word ( const twa_run_ptr &  run)
inline

Create a twa_word from a twa_run.

◆ mask_acc_sets()

twa_graph_ptr spot::mask_acc_sets ( const const_twa_graph_ptr &  in,
acc_cond::mark_t  to_remove 
)

Remove all edges that belong to some given acceptance sets.

◆ mask_keep_accessible_states()

twa_graph_ptr spot::mask_keep_accessible_states ( const const_twa_graph_ptr &  in,
std::vector< bool > &  to_keep,
unsigned int  init,
bool  drop_univ_branches = false 
)

Keep only the states specified by to_keep that are accessible.

Each index in the vector to_keep specifies wether or not to keep the transition that exit this state. The initial state will be set to init. Only states that are accessible from init via states in to_keep will be preserved.

If drop_univ_branches branch is set, universal branching is replaced by existential branching during the copy.

See also
mask_keep_states

◆ mask_keep_states()

twa_graph_ptr spot::mask_keep_states ( const const_twa_graph_ptr &  in,
std::vector< bool > &  to_keep,
unsigned int  init 
)

Keep only the states as specified by to_keep.

Each index in the vector to_keep specifies wether or not to keep the transition that exit this state. The initial state will be set to init.

Note that the number of states in the result automaton is the same as in the input: only transitions have been removed.

See also
mask_keep_accessible_states

◆ memusage()

int spot::memusage ( )

Total number of pages in use by the program.

Returns
The total number of pages in use by the program if known. -1 otherwise.

◆ nesting_depth() [1/3]

unsigned spot::nesting_depth ( formula  f,
const char *  opers 
)

Compute the nesting depth of a set of operators.

Return the maximum number of occurrence of any operator listed opers, among all branches of the AST of f.

Operators to count should be supplied in opers as a string of letters among 'X', 'F', 'G', 'U', 'R', 'M', 'W', '&', '|', '!', 'i' (implication), 'e' (equivalence).

Add letter '~' to force into negative normal form before processing it.

The string should be terminated by '\0' or ']'.

◆ nesting_depth() [2/3]

unsigned spot::nesting_depth ( formula  f,
const op begin,
const op end 
)

Compute the nesting depth of a set of operators.

Return the maximum number of occurrence of any operator between begin and end among all branches of the AST of f.

◆ nesting_depth() [3/3]

unsigned spot::nesting_depth ( formula  f,
op  oper 
)

Compute the nesting depth of an operator.

Return the maximum number of occurrence of oper among all branches of the AST of f.

◆ nsa_to_dca()

twa_graph_ptr spot::nsa_to_dca ( const_twa_graph_ptr  aut,
bool  named_states = false 
)

Converts a nondet Streett-like aut. to a det. co-Büchi aut.

This function calls first nsa_to_nca() in order to retrieve som information and then runs a breakpoint construction. The algorithm is described in section 4 of [5] .

aut The automaton to convert. named_states name each state for easier debugging.

◆ nsa_to_nca()

twa_graph_ptr spot::nsa_to_nca ( const_twa_graph_ptr  aut,
bool  named_states = false,
vect_nca_info *  nca_info = nullptr 
)

Converts a nondet Streett-like aut. to a nondet. co-Büchi aut.

This function works in top of the augmented subset construction algorithm and is described in section 3.1 of [5] .

This implementation is quite different from the described algorithm. It is made to work with automaton with Street-like acceptance (including Büchi).

aut The automaton to convert. named_states name each state for easier debugging. nca_info retrieve information about state visited infinitely often.

◆ operator<<() [1/2]

std::ostream& spot::operator<< ( std::ostream &  os,
const formula f 
)

Print a formula.

◆ operator<<() [2/2]

std::ostream& spot::operator<< ( std::ostream &  os,
const timer dt 
)
inline

Struct used to start and stop both timer and stopwatch clocks.

◆ operator|()

const mc_rvalue spot::operator| ( const mc_rvalue lhs,
const mc_rvalue rhs 
)

This function helps to find the output value from a set of threads that may have different values.

References DEADLOCK, EMPTY, FAILURE, NO_DEADLOCK, NOT_EMPTY, and SUCCESS.

◆ otf_product()

twa_product_ptr spot::otf_product ( const const_twa_ptr &  left,
const const_twa_ptr &  right 
)
inline

on-the-fly TGBA product

◆ otf_product_at()

twa_product_ptr spot::otf_product_at ( const const_twa_ptr &  left,
const const_twa_ptr &  right,
const state left_init,
const state right_init 
)
inline

on-the-fly TGBA product with forced initial states

◆ parse_word()

twa_word_ptr spot::parse_word ( const std::string &  word,
const bdd_dict_ptr &  dict 
)

Parse a twa_word.

The input should have the form

BF;BF;...;BF;cycle{BF;BF;...;BF}

where BF can be any Boolean formula, and the prefix sequence (before cycle{...}) may be empty.

Parameters
wordthe string to parse
dictthe bdd_dict where atomic propositions should be registered

◆ print_formula_props()

std::ostream& spot::print_formula_props ( std::ostream &  out,
const formula f,
bool  abbreviated = false 
)

Print the properties of formula f on stream out.

◆ prop_copy()

void spot::prop_copy ( const const_twa_ptr &  other,
prop_set  p 
)

Copy the properties of another automaton.

Copy the property specified with p from other to the current automaton.

There is no default value for p on purpose. This way any time we add a new property we have to update every call to prop_copy().

See also
prop_set

◆ prop_keep()

void spot::prop_keep ( prop_set  p)

Keep only a subset of properties of the current automaton.

All properties part of a group set to false in p are reset to their default value of trival::maybe().

◆ random_acceptance()

acc_cond::acc_code spot::random_acceptance ( unsigned  n_accs)

Build a random acceptance where each acceptance sets is used once.

◆ randomize()

void spot::randomize ( twa_graph_ptr &  aut,
bool  randomize_states = true,
bool  randomize_edges = true 
)

Randomize a TGBA.

Make a random permutation of the state, and of the edges leaving this state.

This function preserves state names, and highlighted states, but it does not preserve highlighted edges.

◆ reduce_parity()

twa_graph_ptr spot::reduce_parity ( const const_twa_graph_ptr &  aut,
bool  colored = false,
bool  layered = false 
)

Reduce the parity acceptance condition to use a minimal number of colors.

This implements an algorithm derived from the following article, but generalized to all types of parity acceptance. [7]

The kind of parity (min/max) is preserved, but the style (odd/even) may be altered to reduce the number of colors used.

If colored is true, colored automata are output (this is what the above paper assumes). Otherwise, the smallest or highest colors (depending on the parity kind) is removed to simplify the acceptance condition.

If the input uses state-based acceptance, the output will use state-based acceptance as well.

A parity automaton, sometimes called a chain automaton, can be seen as a stack of layers that are alternatively rejecting and accepting. For instance imagine a parity max automaton that is strongly connected. Removing the transitions with the maximal color might leave a few transitions that were not labeled by this maximal color, but that are part of any cycle anymore: those transition could have been colored with the maximal color, since any cycle going through them would have seen the maximal color. (Once your remove this maximal layer, your can define the next layer similarly.)

When layered is true all transition that belong to the same layer receive the same color. When layer is false, only the transition that where used initially to define the layers (i.e, the transition with the maximal color in the previous exemple), get their color adjusted. The other will receive either no color (if colored is false), or a useless color (if colored is true). Here "useless color" means the smallest color for parity max, and the largest color for parity min.

When layered is true, the output of this function is comparable to what acd_transform() would produce. The difference is that this function preserve the kind (min/max) of parity input, while acd_transform() always output a parity min automaton. Additionally, this function needs fewer resources than acd_transform() because it is already known that the input is a parity automaton. In some (historically inaccurate) way, reduce_parity() can be seen as a specialized version of acd_transform().

The reason layered is false by default, is that not introducing colors in place where there where none occasionally help with simulation-based reductions.

◆ reduce_parity_here()

twa_graph_ptr spot::reduce_parity_here ( twa_graph_ptr  aut,
bool  colored = false,
bool  layered = false 
)

Reduce the parity acceptance condition to use a minimal number of colors.

This implements an algorithm derived from the following article, but generalized to all types of parity acceptance. [7]

The kind of parity (min/max) is preserved, but the style (odd/even) may be altered to reduce the number of colors used.

If colored is true, colored automata are output (this is what the above paper assumes). Otherwise, the smallest or highest colors (depending on the parity kind) is removed to simplify the acceptance condition.

If the input uses state-based acceptance, the output will use state-based acceptance as well.

A parity automaton, sometimes called a chain automaton, can be seen as a stack of layers that are alternatively rejecting and accepting. For instance imagine a parity max automaton that is strongly connected. Removing the transitions with the maximal color might leave a few transitions that were not labeled by this maximal color, but that are part of any cycle anymore: those transition could have been colored with the maximal color, since any cycle going through them would have seen the maximal color. (Once your remove this maximal layer, your can define the next layer similarly.)

When layered is true all transition that belong to the same layer receive the same color. When layer is false, only the transition that where used initially to define the layers (i.e, the transition with the maximal color in the previous exemple), get their color adjusted. The other will receive either no color (if colored is false), or a useless color (if colored is true). Here "useless color" means the smallest color for parity max, and the largest color for parity min.

When layered is true, the output of this function is comparable to what acd_transform() would produce. The difference is that this function preserve the kind (min/max) of parity input, while acd_transform() always output a parity min automaton. Additionally, this function needs fewer resources than acd_transform() because it is already known that the input is a parity automaton. In some (historically inaccurate) way, reduce_parity() can be seen as a specialized version of acd_transform().

The reason layered is false by default, is that not introducing colors in place where there where none occasionally help with simulation-based reductions.

◆ relabel_here()

void spot::relabel_here ( twa_graph_ptr &  aut,
relabeling_map *  relmap 
)

replace atomic propositions in an automaton

The relabeling map relmap should have keys that are atomic propositions, and values that are Boolean formulas.

This function is typically used with maps produced by relabel() or relabel_bse().

◆ sat_minimize()

twa_graph_ptr spot::sat_minimize ( twa_graph_ptr  aut,
const char *  opt,
bool  state_based = false 
)

High-level interface to SAT-based minimization.

Minimize the automaton aut, using options opt. These options are given as a comma-separated list of assignments of the form:

states = 10 // synthetize automaton with fixed number of states max-states = 20 // minimize starting from this upper bound acc = "generalized-Buchi 2" acc = "Rabin 3" acc = "same" /* default *‍/ dichotomy = 1 // use dichotomy incr = 1 // use satsolver incrementally to attempt to delete a fixed number of states before starting from scratch incr < 0 // use satsolver incrementally, never restart colored = 1 // build a colored TωA log = "filename"

◆ satone_to_cube()

spot::cube spot::satone_to_cube ( bdd  one,
cubeset cubeset,
std::unordered_map< int, int > &  binder 
)

Transform one truth assignment represented as a BDD into a cube cube passed in parameter. The parameter binder map bdd indexes to cube indexes.

◆ scc_filter()

twa_graph_ptr spot::scc_filter ( const const_twa_graph_ptr &  aut,
bool  remove_all_useless = false,
scc_info given_si = nullptr 
)

Prune unaccepting SCCs and remove superfluous acceptance conditions.

This function will explore the SCCs of the automaton and remove dead SCCs (i.e. SCC that are not accepting, and those with no exit path leading to an accepting SCC).

Additionally, for Generalized Büchi acceptance, this will try to remove useless acceptance conditions. This operation may diminish the number of acceptance condition of the automaton (for instance when two acceptance conditions are always used together we only keep one) but it will never remove all acceptance conditions, even if it would be OK to have zero.

Acceptance conditions on transitions going to rejecting SCCs are all removed. Acceptance conditions going to an accepting SCC and coming from another SCC are only removed if remove_all_useless is set. The default value of remove_all_useless is false because some algorithms (like the degeneralization) will work better if transitions going to an accepting SCC are accepting.

If the input is inherently weak, the output will be a weak automaton with state-based acceptance. The acceptance condition is set to Büchi unless the input was co-Büchi or t (in which case we keep this acceptance).

If given_sm is supplied, the function will use its result without computing a map of its own.

Warning
Calling scc_filter on a TωA that is not inherently weak and has the SBA property (i.e., transitions leaving accepting states are all marked as accepting) may destroy this property. Use scc_filter_states() instead.

◆ scc_filter_states()

twa_graph_ptr spot::scc_filter_states ( const const_twa_graph_ptr &  aut,
bool  remove_all_useless = false,
scc_info given_si = nullptr 
)

Prune unaccepting SCCs.

This is an abridged version of scc_filter(), that preserves state-based acceptance. I.e., if the input TωA has the SBA property, (i.e., transitions leaving accepting states are all marked as accepting), then the output TωA will also have that property.

◆ scc_filter_susp()

twa_graph_ptr spot::scc_filter_susp ( const const_twa_graph_ptr &  aut,
bool  remove_all_useless,
bdd  suspvars,
bdd  ignoredvars,
bool  early_susp,
scc_info given_si = nullptr 
)

Prune unaccepting SCCs, superfluous acceptance sets, and suspension variables.

In addition to removing useless states, and acceptance sets, this remove all ignoredvars occurring in conditions, and all suspvars in conditions leadings to non-accepting SCC (as well as the conditions between two SCCs if early_susp is false).

This is used by compsusp(), and is probably useless for any other use.

◆ semidet_sccs()

std::vector<bool> spot::semidet_sccs ( scc_info si)

Whether an SCC is in the deterministic part of an automaton.

◆ tba_determinize()

twa_graph_ptr spot::tba_determinize ( const const_twa_graph_ptr &  aut,
unsigned  threshold_states = 0,
unsigned  threshold_cycles = 0 
)

Determinize a TBA using the powerset construction.

The input automaton should have at most one acceptance condition. Beware that not all Büchi automata can be determinized, and this procedure does not ensure that the produced automaton is equivalent to aut.

The construction is adapted from Section 3.2 of [15] only adapted to work on TBA rather than BA.

If threshold_states is non null, abort the construction whenever it would build an automaton that is more than threshold_states time bigger (in term of states) than the original automaton.

If threshold_cycles is non null, abort the construction whenever an SCC of the constructed automaton has more than threshold_cycles cycles.

◆ tba_determinize_check()

twa_graph_ptr spot::tba_determinize_check ( const twa_graph_ptr &  aut,
unsigned  threshold_states = 0,
unsigned  threshold_cycles = 0,
formula  f = nullptr,
const_twa_graph_ptr  neg_aut = nullptr 
)

Determinize a TBA and make sure it is correct.

Apply tba_determinize(), then check that the result is equivalent. If it isn't, return the original automaton.

Only one of f or neg_aut needs to be supplied. If neg_aut is not given, it will be built from f.

Parameters
autthe automaton to minimize
threshold_statesif non null, abort the construction whenever it would build an automaton that is more than threshold time bigger (in term of states) than the original automaton.
threshold_cyclescan be used to abort the construction if the number of cycles in a SCC of the constructed automaton is bigger than the supplied value.
fthe formula represented by the original automaton
neg_autan automaton representing the negation of aut
Returns
a new tgba if the automaton could be determinized, aut if the automaton cannot be determinized, 0 if we do not know if the determinization is correct because neither f nor neg_aut were supplied.

◆ to_dca()

twa_graph_ptr spot::to_dca ( const_twa_graph_ptr  aut,
bool  named_states = false 
)

Converts any ω-automata to deterministic co-buchi.

The language of the resulting automaton always include the original language, and is a superset iff the original language can not be expressed using a co-Büchi acceptance condition.

The implementation dispatches between dnf_to_dca, nsa_to_dca, degeneralize(), and a trivial implementation for deterministic weak automata.

◆ to_finite()

twa_graph_ptr spot::to_finite ( const_twa_graph_ptr  aut,
const char *  alive = "alive" 
)

Interpret the "live" part of an automaton as finite automaton.

This functions assumes that there is a property "alive" is that either true or false on all transitions, and that can only switch from true to false.

Because Spot does not support finite automata, this creates a state-based Büchi automaton where any states with a !alive outgoing transition in the original automaton is accepting, and all alive/!alive occurrences are removed.

◆ to_nca()

twa_graph_ptr spot::to_nca ( const_twa_graph_ptr  aut,
bool  named_states = false 
)

Converts any ω-automata to non-deterministic co-buchi.

The language of the resulting automaton always include the original language, and is a superset iff the original language can not be expressed using a co-Büchi acceptance condition.

The implementation dispatches between dnf_to_nca(), nsa_to_nca(), degeneralize_tba(), and a trivial implementation for weak automata.

◆ to_weak_alternating()

twa_graph_ptr spot::to_weak_alternating ( const_twa_graph_ptr &  aut,
bool  less = false 
)

Convert an alternating automaton to a weak alternating automaton.

 

The input automaton must have a generalized co-Büchi or Büchi acceptance condition. The automaton will be converted into a weak Büchi automaton. If the input automaton is already weak, it will simply be copied.

For details about the algorithm used, see the following papers: [33] , [35] .

Although at the end of the above paper there is a hint at an optimization that greatly reduces the number of transition in the resulting automaton, but in return makes the run of remove_alternation algorithm way slower. Hence, the optimization is disabled by default.

Parameters
autthe automaton to convert to weak
lesswhether to activate the optimization on the number of transitions or not, disabled by default

◆ transform_accessible()

template<typename Trans >
void spot::transform_accessible ( const const_twa_graph_ptr &  old,
twa_graph_ptr &  cpy,
Trans  trans,
unsigned int  init,
bool  drop_univ_branches = false 
)

Clone and mask an automaton.

Copy the edges of automaton old into the empty automaton cpy, creating new states as needed. The argument trans should behave as a function with the following prototype: void (*trans) (unsigned src, bdd& cond, acc_cond::mark_t& acc, unsigned dst)

The trans function may modify either the condition or the acceptance sets of the edges. Set the condition to bddfalse to remove the edge (this will also remove the destination state and its descendants if they are not reachable by another edge).

The mapping between each state of the resulting automaton and the original state of the input automaton is stored in the "original-states" named property of the produced automaton. Call aut->get_named_prop<std::vector<unsigned>>("original-states") to retrieve it.

If drop_univ_branches branch is set, universal branching is replaced by existential branching during the copy.

Parameters
initThe optional new initial state.

◆ transform_copy()

template<typename Trans >
void spot::transform_copy ( const const_twa_graph_ptr &  old,
twa_graph_ptr &  cpy,
Trans  trans,
unsigned int  init 
)

Copy an automaton and update each edge.

Copy the states of automaton old, into automaton cpy. Each state in cpy will have the same id as the ones in old. The argument trans should behave as a function with the following prototype: void (*trans) (unsigned srcbdd& cond, acc_cond::mark_t& acc, unsigned dst) It can modify either the condition or the acceptance sets of the edges. Set the condition to bddfalse to remove it. Note that all transtions will be processed.

Parameters
initThe optional new initial state.

◆ twa_to_twacube()

twacube_ptr spot::twa_to_twacube ( spot::const_twa_graph_ptr  aut)

Convert a twa into a twacube.

◆ twacube_to_twa()

spot::twa_graph_ptr spot::twacube_to_twa ( spot::twacube_ptr  twacube,
spot::bdd_dict_ptr  d = nullptr 
)

Convert a twacube into a twa. When \d is specified, the BDD_dict in parameter is used rather than creating a new one.


Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.9.1