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
141
|
/* presburger_transduction.c - DFA package example application */
/*
* MONA
* Copyright (C) 1997-2013 Aarhus University.
*
* This program is free software; you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation; either version 2 of the License, or
* (at your option) any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program; if not, write to the Free Software
* Foundation, Inc., 51 Franklin Street, Suite 500, Boston, MA 02110-1335,
* USA.
*/
/* This example illustrates how to use transduction and
* iteration. It constructs an automaton for 'p_index = value'
* using Presburger encoding by starting with an automaton
* for the relation 'p_i = 1' and iteratively adding 1
* to the constant using projection, product and index-replacing.
* (This is not supposed to be an efficient way of
* constructing these automata - the purpuse is to illustrate
* the iterative approach.)
*/
#define INDEX 7
#define VALUE 13
#include <stdio.h>
#include <stdlib.h>
#include "dfa.h"
#include "mem.h"
int main()
{
DFA *a1, *a2, *a3, *a4, *a5, *a6, *a7, *a8, *a9;
int i;
/* initialize the BDD package */
bdd_init();
/* import the 'presburger_plus_012.dfa' automaton
generated by running 'mona presburger.mona' */
{
char **vars; /* 0 terminated array of variable names */
int *orders; /* array of variable orders (0/1/2) */
a1 = dfaImport("presburger_plus_012.dfa", &vars, &orders);
if (!a1) {
printf("error: unable to read 'presburger_plus_012.dfa' "
"(run 'mona -n presburger.mona')\n");
exit(-1);
}
/* 'vars' now contains {"p","q","r"}, i.e. the variables in their
original index ordering, 'orders' contains {2,2,2} */
for (i = 0; vars[i]; i++)
mem_free(vars[i]);
mem_free(vars);
mem_free(orders);
}
/* make automaton for 'p_1 = 1' */
a2 = dfaPresbConst(1, 1);
/* make the intersection product of 'a1' and 'a2'
and project(+right-quotient) 'p_1' away -
this corresponds to making an automaton for the
following formula: 'ex p_1: p_0 + p_1 = p_2 & p_1 = 1' */
a3 = dfaProduct(a1, a2, dfaAND);
a4 = dfaMinimize(a3);
dfaRightQuotient(a4, 1);
a5 = dfaProject(a4, 1);
a6 = dfaMinimize(a5);
/* a6 now represents the formula 'p_0 + 1 = p_2' */
/* clean up the temporary automata */
dfaFree(a1);
dfaFree(a3);
dfaFree(a4);
dfaFree(a5);
/* for the base case of the iteration, we need an automaton
for 'p_0 = 1' - reuse a2 by replacing the index */
{
int map[2];
map[1] = 0; /* means: replace 1 with 0 in all BDD nodes */
dfaReplaceIndices(a2, map);
}
/* the main part: iterate the transduction */
for (i = 1; i < VALUE; i++) {
/* make an automaton for 'ex p_0: p_0 = i & p_0 + 1 = p_2' */
a7 = dfaProduct(a6, a2, dfaAND);
a8 = dfaMinimize(a7);
dfaRightQuotient(a8, 0);
a9 = dfaProject(a8, 0);
/* make automaton for 'p_0 = i+1' by a replace-indices */
{
int map[3];
map[2] = 0;
dfaReplaceIndices(a9, map);
}
/* clean up */
dfaFree(a7);
dfaFree(a8);
dfaFree(a2);
a2 = a9;
/* now a2 represents 'p_0 = i+1' */
}
/* clean up */
dfaFree(a6);
/* set the index */
{
int map[1];
map[0] = INDEX;
dfaReplaceIndices(a2, map);
}
/* output the resulting automaton in Graphviz format */
{
unsigned indices[1]; /* array of indices in alphabet */
indices[0] = INDEX;
dfaPrintGraphviz(a2, 1, indices);
}
dfaFree(a2);
return 0;
}
|
