spot  2.9.8
ltsmin.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2011, 2013-2016, 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/kripke/kripke.hh>
23 #include <spot/tl/apcollect.hh>
24 
25 namespace spot
26 {
27  struct spins_interface;
28 
29  class SPOT_API ltsmin_model final
30  {
31  public:
32  ~ltsmin_model();
33 
34  // \brief Load an ltsmin model, either from divine or promela.
35  //
36  // The filename given can be either a *.pm/*.pml/*.prom promela
37  // source or a *.spins dynamic library compiled with "spins file".
38  // If a promela source is supplied, this function will call spins to
39  // update the *.spins library only if it is not newer.
40  //
41  // Similarly the divine models can be specified as *.dve source or
42  // *.dve or *.dve2C libraries.
43  //
44  static ltsmin_model load(const std::string& file);
45 
46  // \brief Generate a Kripke structure on-the-fly
47  //
48  // The dead parameter is used to control the behavior of the model
49  // on dead states (i.e. the final states of finite sequences). If
50  // DEAD is formula::ff(), it means we are not interested in finite
51  // sequences of the system, and dead state will have no successor.
52  // If DEAD is formula::tt(), we want to check finite sequences as
53  // well as infinite sequences, but do not need to distinguish
54  // them. In that case dead state will have a loop labeled by
55  // true. If DEAD is any atomic proposition (formula::ap("...")),
56  // this is the name a property that should be true when looping on
57  // a dead state, and false otherwise.
58  //
59  // This function returns nullptr on error.
60  //
61  // \a to_observe the list of atomic propositions that should be observed
62  // in the model
63  // \a dict the BDD dictionary to use
64  // \a dead an atomic proposition or constant to use for looping on
65  // dead states
66  // \a compress whether to compress the states. Use 0 to disable, 1
67  // to enable compression, 2 to enable a faster compression that only
68  // work if all variables are smaller than 2^28.
69  kripke_ptr kripke(const atomic_prop_set* to_observe,
70  bdd_dict_ptr dict,
71  formula dead = formula::tt(),
72  int compress = 0) const;
73 
75  int state_size() const;
77  const char* state_variable_name(int var) const;
79  int state_variable_type(int var) const;
81  int type_count() const;
83  const char* type_name(int type) const;
85  int type_value_count(int type);
87  const char* type_value_name(int type, int val);
88 
89  private:
90  ltsmin_model(std::shared_ptr<const spins_interface> iface) : iface(iface)
91  {
92  }
93  std::shared_ptr<const spins_interface> iface;
94  };
95 }
Definition: automata.hh:26
Definition: ltsmin.hh:29
Interface for a Kripke structure.
Definition: kripke.hh:90
static formula tt()
Return the true constant.
Definition: formula.hh:1514
Main class for temporal logic formula.
Definition: formula.hh:714
std::set< formula > atomic_prop_set
Set of atomic propositions.
Definition: apcollect.hh:36

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.8.13