spot 2.11.1.dev
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
29namespace spot
30{
31 class SPOT_API ltsmin_model final
32 {
33 public:
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:715
static formula tt()
Return the true constant.
Definition: formula.hh:1514
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_value_name(int type, int val)
Name of each enumerated value for a 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_name(int type) const
Name of each 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.4