spot 2.12.2
tgtaproduct.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/twa/twa.hh>
22#include <spot/twa/twaproduct.hh>
23#include <spot/misc/fixpool.hh>
24#include <spot/kripke/kripke.hh>
25#include <spot/ta/tgta.hh>
26
27namespace spot
28{
29
31 class SPOT_API tgta_product : public twa_product
32 {
33 public:
34 tgta_product(const const_kripke_ptr& left,
35 const const_tgta_ptr& right);
36
37 virtual const state* get_init_state() const override;
38
39 virtual twa_succ_iterator*
40 succ_iter(const state* local_state) const override;
41 };
42
43 inline twa_ptr product(const const_kripke_ptr& left,
44 const const_tgta_ptr& right)
45 {
46 return std::make_shared<tgta_product>(left, right);
47 }
48
50 class SPOT_API tgta_succ_iterator_product final : public twa_succ_iterator
51 {
52 public:
54 const const_kripke_ptr& k,
55 const const_tgta_ptr& tgta,
57
58 virtual
60
61 // iteration
62 bool first() override;
63 bool next() override;
64 bool done() const override;
65
66 // inspection
67 state_product* dst() const override;
68 bdd cond() const override;
69 acc_cond::mark_t acc() const override;
70
71 private:
73
74 void
75 step_();
76 bool find_next_succ_();
77
78 void
79 next_kripke_dest();
80
82
83 protected:
84 const state_product* source_;
85 const_tgta_ptr tgta_;
86 const_kripke_ptr kripke_;
88 twa_succ_iterator* tgta_succ_it_;
89 twa_succ_iterator* kripke_succ_it_;
90 state_product* current_state_;
91 bdd current_condition_;
92 acc_cond::mark_t current_acceptance_conditions_;
93 bdd kripke_source_condition;
94 const state* kripke_current_dest_state;
95 };
96}
A state for spot::twa_product.
Definition: twaproduct.hh:33
Abstract class for states.
Definition: twa.hh:47
A lazy product. (States are computed on the fly.)
Definition: tgtaproduct.hh:32
virtual const state * get_init_state() const override
Get the initial state of the automaton.
virtual twa_succ_iterator * succ_iter(const state *local_state) const override
Get an iterator over the successors of local_state.
Iterate over the successors of a product computed on the fly.
Definition: tgtaproduct.hh:51
bool done() const override
Check whether the iteration is finished.
bdd cond() const override
Get the condition on the edge leading to this successor.
acc_cond::mark_t acc() const override
Get the acceptance mark of the edge leading to this successor.
bool next() override
Jump to the next successor (if any).
bool first() override
Position the iterator on the first successor (if any).
state_product * dst() const override
Get the destination state of the current edge.
A Transition-based Generalized Testing Automaton (TGTA).
Definition: tgta.hh:59
A lazy product. (States are computed on the fly.)
Definition: twaproduct.hh:79
Iterate over the successors of a state.
Definition: twa.hh:394
Definition: automata.hh:26
An acceptance mark.
Definition: acc.hh:84

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