spot  2.11.6
ltsmin.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2011, 2013-2016, 2017, 2019 Laboratoire de Recherche et
3 // Developpement de l'Epita (LRDE)
4 //
5 // This file is part of Spot, a model checking library.
6 //
7 // Spot is free software; you can redistribute it and/or modify it
8 // under the terms of the GNU General Public License as published by
9 // the Free Software Foundation; either version 3 of the License, or
10 // (at your option) any later version.
11 //
12 // Spot is distributed in the hope that it will be useful, but WITHOUT
13 // ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
14 // or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
15 // License for more details.
16 //
17 // You should have received a copy of the GNU General Public License
18 // along with this program. If not, see <http://www.gnu.org/licenses/>.
19 
20 #pragma once
21 
22 #include <spot/ltsmin/spins_interface.hh>
23 #include <spot/ltsmin/spins_kripke.hh>
24 #include <spot/kripke/kripke.hh>
25 #include <spot/twacube/twacube.hh>
26 #include <spot/tl/apcollect.hh>
27 #include <tuple>
28 
29 namespace spot
30 {
31  class SPOT_API ltsmin_model final
32  {
33  public:
34  ~ltsmin_model();
35 
36  // \brief Load an ltsmin model, either from divine or promela.
37  //
38  // The filename given can be either a *.pm/*.pml/*.prom promela
39  // source or a *.spins dynamic library compiled with "spins file".
40  // If a promela source is supplied, this function will call spins to
41  // update the *.spins library only if it is not newer.
42  //
43  // Similarly the divine models can be specified as *.dve source or
44  // *.dve or *.dve2C libraries.
45  //
46  static ltsmin_model load(const std::string& file);
47 
48  // \brief Generate a Kripke structure on-the-fly
49  //
50  // The dead parameter is used to control the behavior of the model
51  // on dead states (i.e. the final states of finite sequences). If
52  // DEAD is formula::ff(), it means we are not interested in finite
53  // sequences of the system, and dead state will have no successor.
54  // If DEAD is formula::tt(), we want to check finite sequences as
55  // well as infinite sequences, but do not need to distinguish
56  // them. In that case dead state will have a loop labeled by
57  // true. If DEAD is any atomic proposition (formula::ap("...")),
58  // this is the name a property that should be true when looping on
59  // a dead state, and false otherwise.
60  //
61  // This function returns nullptr on error.
62  //
63  // \a to_observe the list of atomic propositions that should be observed
64  // in the model
65  // \a dict the BDD dictionary to use
66  // \a dead an atomic proposition or constant to use for looping on
67  // dead states
68  // \a compress whether to compress the states. Use 0 to disable, 1
69  // to enable compression, 2 to enable a faster compression that only
70  // work if all variables are smaller than 2^28.
71  kripke_ptr kripke(const atomic_prop_set* to_observe,
72  bdd_dict_ptr dict,
73  formula dead = formula::tt(),
74  int compress = 0) const;
75 
76  // \brief The same as above but returns a kripkecube, i.e. a kripke
77  // that can be use in parallel. Moreover, it support more ellaborated
78  // atomic propositions such as "P.a == P.c"
79  ltsmin_kripkecube_ptr kripkecube(std::vector<std::string> to_observe,
80  formula dead = formula::tt(),
81  int compress = 0,
82  unsigned int nb_threads = 1) const;
83 
85  int state_size() const;
87  const char* state_variable_name(int var) const;
89  int state_variable_type(int var) const;
91  int type_count() const;
93  const char* type_name(int type) const;
95  int type_value_count(int type);
97  const char* type_value_name(int type, int val);
98 
99  private:
100  ltsmin_model(std::shared_ptr<const spins_interface> iface) : iface(iface)
101  {
102  }
103  std::shared_ptr<const spins_interface> iface;
104  };
105 }
Main class for temporal logic formula.
Definition: formula.hh:717
static formula tt()
Return the true constant.
Definition: formula.hh:1516
Interface for a Kripke structure.
Definition: kripke.hh:178
This class is a template representation of a Kripke structure. It is composed of two template paramet...
Definition: kripke.hh:41
Definition: ltsmin.hh:32
const char * type_name(int type) const
Name of each type.
int type_value_count(int type)
Count of enumerated values for a type.
int type_count() const
Number of different types.
const char * type_value_name(int type, int val)
Name of each enumerated value for a type.
int state_variable_type(int var) const
Type of each variable.
const char * state_variable_name(int var) const
Name of each variable.
int state_size() const
Number of variables in a state.
std::set< formula > atomic_prop_set
Set of atomic propositions.
Definition: apcollect.hh:36
Definition: automata.hh:27
std::shared_ptr< spot::kripkecube< spot::cspins_state, spot::cspins_iterator > > ltsmin_kripkecube_ptr
shortcut to manipulate the kripke below
Definition: spins_kripke.hh:257

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