1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
|
#include <iostream>
#include <queue>
#include <string>
#include "mcrl2/lps/next_state_generator_old.h"
using namespace mcrl2;
void traverse_states(const lps::specification& lps_spec, bool per_summand = false)
{
using namespace mcrl2::lps;
next_state_generator generator(lps_spec, data::jitty_compiling);
atermpp::aterm initial_state = generator.initial_state();
std::set<atermpp::aterm> visited;
std::set<atermpp::aterm> seen;
std::set<atermpp::aterm_appl> transition_labels;
size_t transitions = 0;
std::queue<atermpp::aterm, std::deque<atermpp::aterm> > q;
q.push(initial_state);
seen.insert(initial_state);
while (!q.empty())
{
visited.insert(q.front());
if (per_summand)
{
for (size_t i = 0; i < lps_spec.process().summand_count(); ++i)
{
next_state_generator::iterator first = generator.begin(q.front(), i);
while (++first)
{
const next_state_generator::state_type& s = *first;
transition_labels.insert(s.transition);
++transitions;
if (seen.find(s.state) == seen.end())
{
q.push(s.state);
seen.insert(s.state);
}
}
}
}
else
{
next_state_generator::iterator first = generator.begin(q.front());
while (++first)
{
const next_state_generator::state_type& s = *first;
transition_labels.insert(s.transition);
++transitions;
if (seen.find(s.state) == seen.end())
{
q.push(s.state);
seen.insert(s.state);
}
}
}
q.pop();
}
std::cout << "visited " << visited.size() << " states" << std::endl;
}
int main(int argc, char* argv[])
{
if (argc != 2)
{
mCRL2log(log::warning) << "usage: next_state_generator LPS_FILE" << std::endl;
}
else
{
std::string filename(argv[1]);
std::cout << "loading LPS from file " << filename << std::endl;
lps::specification spec;
spec.load(filename);
std::cout << "traversing states..." << std::endl;
traverse_states(spec);
}
return 0;
}
|
