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

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