/
soundness.c
140 lines (121 loc) · 3.5 KB
/
soundness.c
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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
#include <cassert>
#include <map>
#include <spot/twaalgos/determinize.hh>
#include <spot/twaalgos/complement.hh>
#include <spot/twaalgos/totgba.hh>
#include <spot/twaalgos/copy.hh>
#include <spot/twaalgos/stutter.hh>
#include <spot/twa/twaproduct.hh>
#include <spot/twaalgos/gtec/gtec.hh>
#include <spot/twaalgos/dot.hh>
#include <spot/twaalgos/remfin.hh>
#include <iostream>
extern "C" {
#include <memory.h>
#include <mlvalues.h>
}
#include "proof_aut.hpp"
#include "trace.hpp"
static std::shared_ptr<ProofAutomaton> proof = 0;
static std::map< int, Vertex > bdd_map;
extern "C" void create_aut(value max_log2_states) {
CAMLparam1(max_log2_states);
// std::cerr << "create_aut " << Int_val(max_log2_states) << '\n';
assert(proof==0);
proof = std::make_shared<ProofAutomaton>(Int_val(max_log2_states));
CAMLreturn0;
}
extern "C" void destroy_aut() {
CAMLparam0();
// std::cerr << "destroy_aut\n";
assert(proof);
proof = 0;
bdd_map.clear();
CAMLreturn0;
}
//extern "C" value create_tag() {
// CAMLparam0();
// CAMLlocal1(v_res);
// assert(proof);
// v_res = Val_int(proof->create_tag());
// CAMLreturn(v_res);
//}
extern "C" void create_vertex(value v_) {
CAMLparam1(v_);
assert(proof);
Vertex v = proof->create_vertex();
int id = Int_val(v_); //v.id();
assert( bdd_map.find(id) == bdd_map.end() );
bdd_map[id] = v;
// std:: cerr << "create_vertex " << id << '\n';
CAMLreturn0;
}
extern "C" void tag_vertex(value v_, value t_) {
CAMLparam2(v_, t_);
int v = Int_val(v_);
Tag t = Int_val(t_);
assert(proof);
assert( bdd_map.find(v) != bdd_map.end() );
proof->tag_vertex(bdd_map[v], t);
CAMLreturn0;
}
extern "C" void set_successor(value v1_, value v2_) {
CAMLparam2(v1_, v2_);
int v1 = Int_val(v1_);
int v2 = Int_val(v2_);
assert(proof);
assert( bdd_map.find(v1) != bdd_map.end() );
assert( bdd_map.find(v2) != bdd_map.end() );
proof->set_successor(bdd_map[v1], bdd_map[v2]);
CAMLreturn0;
}
extern "C" void set_trace_pair(value v1_, value v2_, value t1_, value t2_) {
CAMLparam4(v1_, v2_, t1_, t2_);
int v1 = Int_val(v1_);
int v2 = Int_val(v2_);
Tag t1 = Int_val(t1_);
Tag t2 = Int_val(t2_);
assert(proof);
assert( bdd_map.find(v1) != bdd_map.end() );
assert( bdd_map.find(v2) != bdd_map.end() );
proof->set_trace_pair(bdd_map[v1], bdd_map[v2], t1, t2);
CAMLreturn0;
}
extern "C" void set_progress_pair(value v1_, value v2_, value t1_, value t2_) {
CAMLparam4(v1_, v2_, t1_, t2_);
int v1 = Int_val(v1_);
int v2 = Int_val(v2_);
Tag t1 = Int_val(t1_);
Tag t2 = Int_val(t2_);
assert(proof);
assert( bdd_map.find(v1) != bdd_map.end() );
assert( bdd_map.find(v2) != bdd_map.end() );
proof->set_progress_pair(bdd_map[v1], bdd_map[v2], t1, t2);
CAMLreturn0;
}
extern "C" value check_soundness() {
CAMLparam0();
CAMLlocal1(v_res);
spot::const_twa_ptr ta = std::make_shared<TraceAutomaton>(*proof);
spot::twa_graph_ptr graph = copy(ta, spot::twa::prop_set::all());
spot::twa_graph_ptr det =
tgba_determinize(
graph, false, true, true,
spot::check_stutter_invariance(graph).is_true()
);
spot::twa_graph_ptr complement = remove_fin(dtwa_complement(det));
spot::const_twa_ptr product = otf_product(proof, complement);
bool retval = (product->is_empty());
//std:: cout << "retval " << retval << '\n';
v_res = Val_bool(retval);
CAMLreturn(v_res);
}
extern "C" void set_initial_vertex(value v_) {
CAMLparam1(v_);
int v = Int_val(v_);
// std::cerr << "set_initial_vertex " << v << '\n';
assert(proof);
assert( bdd_map.find(v) != bdd_map.end() );
proof->set_initial_vertex( bdd_map[v] );
CAMLreturn0;
}