spot  2.4.2
ltsmin.hh
1 // -*- coding: utf-8 -*-
2 // Copyright (C) 2011, 2013, 2014, 2015, 2016 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).
50  // If DEAD is "false", it means we are not
51  // interested in finite sequences of the system, and dead state
52  // will have no successor. If DEAD is
53  // "true", we want to check finite sequences as well as infinite
54  // sequences, but do not need to distinguish them. In that case
55  // dead state will have a loop labeled by true. If DEAD is any
56  // other string, this is the name a property that should be true
57  // when looping on a dead state, and false otherwise.
58  //
59  // This function returns 0 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:1370
Main class for temporal logic formula.
Definition: formula.hh:673
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 Sat Nov 25 2017 02:13:16 for spot by doxygen 1.8.13