blob: 41b8ef8640c4c25f84580e5b8ff6c97ec614f93b (
plain)
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
|
/* FIXME: Finer imports */
import kodkod.ast.*;
import kodkod.engine.*;
import kodkod.engine.config.*;
import kodkod.engine.satlab.*;
import kodkod.instance.*;
public class Main
{
private static Parameters PARAMETERS;
private static VHDLModel MODEL;
private static VariableManager VARIABLE_MANAGER;
public static VHDLModel get_model ()
{
return MODEL;
}
public static VariableManager get_variable_manager ()
{
return VARIABLE_MANAGER;
}
private static Formula get_formula (final VHDLModel model)
{
final Variable w;
w = Variable.unary("w");
return
w.join
(
model.get_predicate_as_relation("is_accessed_by")
).no().forSome(w.oneOf(model.get_type_as_relation("waveform")));
}
public static void main (final String... args)
{
/*
* Order of operations:
* 1/ Load Levels (Types + predicates)
* 2/ Load Properties (will change 'is_used()' on predicates)
* 3/ Generate complementary model according to used predicates.
* 4/ Load Model, but only for used predicates and types.
* 5/ Add all used types and predicates to the Universe.
*/
final Universe univ;
final TupleFactory tf;
final Bounds bounds;
final Solver solver;
final Solution sol;
final Formula property;
PARAMETERS = new Parameters(args);
if (!PARAMETERS.are_valid())
{
return;
}
VARIABLE_MANAGER = new VariableManager(PARAMETERS.get_variables_prefix());
MODEL = new VHDLModel();
/* 1/ Load Levels (Types + predicates) */
try
{
VHDLLevel.add_to_model
(
MODEL,
(
PARAMETERS.get_levels_directory()
+ "/structural_level.data"
)
);
}
catch (final Exception e)
{
System.err.println("[E] Could not load structural level:");
e.printStackTrace();
return;
}
/* 2/ Load Properties (will change 'is_used()' on predicates) */
property = get_formula(MODEL);
/* TODO */
/* 3/ Generate complementary model according to used predicates. */
/* TODO */
/* 4/ Load Model, but only for used predicates and types. */
try
{
MODEL.parse_file(PARAMETERS.get_model_file());
}
catch (final Exception e)
{
System.err.println("[E] Could not load instructions:");
e.printStackTrace();
return;
}
/* 5/ Add all types and used predicates to the Universe. */
univ = new Universe(MODEL.get_atoms());
tf = univ.factory();
bounds = new Bounds(univ);
MODEL.add_to_bounds(bounds, tf);
solver = new Solver();
solver.options().setSolver(SATFactory.DefaultSAT4J);
solver.options().setReporter(new ConsoleReporter());
sol = solver.solve(property, bounds);
System.out.println(sol);
}
}
|
