Imported Upstream version 1.2.1
Ralf Treinen
13 years ago
| 0 | // -*- c++ -*- | |
| 1 | /// @file BitVector.C | |
| 2 | ||
| 3 | #ifdef __GNUC__ | |
| 4 | # pragma implementation | |
| 5 | #endif // __GNUC__ | |
| 6 | #include "BitVector.h" |
| 0 | // -*- c++ -*- | |
| 1 | /// @file BitVector.h | |
| 2 | /* | |
| 3 | * Copyright © 2001 Marko Mäkelä <msmakela@tcs.hut.fi> | |
| 4 | * | |
| 5 | * This program is free software; you can redistribute it and/or | |
| 6 | * modify it under the terms of the GNU General Public License | |
| 7 | * as published by the Free Software Foundation; either version 2 | |
| 8 | * of the License, or (at your option) any later version. | |
| 9 | * | |
| 10 | * This program is distributed in the hope that it will be useful, | |
| 11 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
| 12 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
| 13 | * GNU General Public License for more details. | |
| 14 | * | |
| 15 | * You should have received a copy of the GNU General Public License | |
| 16 | * along with this program; if not, write to the Free Software | |
| 17 | * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. | |
| 18 | */ | |
| 19 | ||
| 20 | #ifndef BITVECTOR_H_ | |
| 21 | # define BITVECTOR_H_ | |
| 22 | # ifdef __GNUC__ | |
| 23 | # pragma interface | |
| 24 | # endif // __GNUC__ | |
| 25 | ||
| 26 | # include <limits.h> | |
| 27 | # include <string.h> | |
| 28 | ||
| 29 | /** Binary digit (bit) vector */ | |
| 30 | class BitVector | |
| 31 | { | |
| 32 | public: | |
| 33 | /** machine word */ | |
| 34 | typedef unsigned long word_t; | |
| 35 | ||
| 36 | /** Constructor | |
| 37 | * @param size number of elements in the vector | |
| 38 | */ | |
| 39 | explicit BitVector (unsigned size = 0) : | |
| 40 | m_size (0), m_allocated (1), m_bits (new word_t[1]) { | |
| 41 | *m_bits = 0; | |
| 42 | setSize (size); | |
| 43 | } | |
| 44 | /** Copy constructor */ | |
| 45 | explicit BitVector (const class BitVector& old) : | |
| 46 | m_size (old.m_size), m_allocated (old.m_allocated), m_bits (0) { | |
| 47 | memcpy (m_bits = new word_t[m_allocated], old.m_bits, | |
| 48 | m_allocated * sizeof (word_t)); | |
| 49 | } | |
| 50 | private: | |
| 51 | /** Assignment operator */ | |
| 52 | class BitVector& operator= (const class BitVector& old); | |
| 53 | public: | |
| 54 | /** Destructor */ | |
| 55 | ~BitVector () { delete[] m_bits; } | |
| 56 | ||
| 57 | /** Equality comparison | |
| 58 | * @param other other bit vector to compare this against | |
| 59 | * @return true if the bit vectors are identical, | |
| 60 | * treating missing bits as unset | |
| 61 | */ | |
| 62 | bool operator== (const class BitVector& other) const { | |
| 63 | unsigned tsize = getNumWords (m_size), osize = getNumWords (other.m_size); | |
| 64 | if (tsize < osize) { | |
| 65 | if (memcmp (m_bits, other.m_bits, tsize * sizeof (word_t))) | |
| 66 | return false; | |
| 67 | for (register const word_t* bits = other.m_bits + osize; | |
| 68 | bits-- > other.m_bits + tsize; ) | |
| 69 | if (*bits) | |
| 70 | return false; | |
| 71 | } | |
| 72 | else { | |
| 73 | if (memcmp (m_bits, other.m_bits, osize * sizeof (word_t))) | |
| 74 | return false; | |
| 75 | for (register const word_t* bits = m_bits + tsize; | |
| 76 | bits-- > m_bits + osize; ) | |
| 77 | if (*bits) | |
| 78 | return false; | |
| 79 | } | |
| 80 | return true; | |
| 81 | } | |
| 82 | ||
| 83 | /** Determine the number of words the specified amount of bits occupy */ | |
| 84 | static unsigned getNumWords (unsigned bits) { | |
| 85 | const unsigned bitsPerWord = CHAR_BIT * sizeof (word_t); | |
| 86 | return (bits + bitsPerWord - 1) / bitsPerWord; | |
| 87 | } | |
| 88 | ||
| 89 | /** Set the size of the vector | |
| 90 | * @param size the new size of the vector | |
| 91 | */ | |
| 92 | void setSize (unsigned size) { | |
| 93 | const unsigned numWords = getNumWords (size); | |
| 94 | if (m_allocated < numWords) { | |
| 95 | while (m_allocated < numWords) | |
| 96 | m_allocated <<= 1; | |
| 97 | word_t* bits = new word_t[m_allocated]; | |
| 98 | const unsigned init = getNumWords (m_size); | |
| 99 | memcpy (bits, m_bits, init * sizeof *m_bits); | |
| 100 | memset (bits + init, 0, (m_allocated - init) * sizeof *m_bits); | |
| 101 | delete[] m_bits; | |
| 102 | m_bits = bits; | |
| 103 | } | |
| 104 | m_size = size; | |
| 105 | } | |
| 106 | /** Determine the size of the vector | |
| 107 | * @return the size of the vector | |
| 108 | */ | |
| 109 | unsigned getSize () const { return m_size; } | |
| 110 | ||
| 111 | /** Read a binary digit | |
| 112 | * @param i zero-based index of the element | |
| 113 | * @return value of the ternary digit | |
| 114 | */ | |
| 115 | bool operator[] (unsigned i) const { | |
| 116 | return i < m_size && | |
| 117 | m_bits[i / (CHAR_BIT * sizeof (word_t))] & | |
| 118 | (word_t (1) << (i % (CHAR_BIT * sizeof (word_t)))); | |
| 119 | } | |
| 120 | ||
| 121 | /** Set a binary digit | |
| 122 | * @param i zero-based index of the element | |
| 123 | */ | |
| 124 | void assign_true (unsigned i) { | |
| 125 | if (i >= m_size) | |
| 126 | setSize (i + 1); | |
| 127 | m_bits[i / (CHAR_BIT * sizeof (word_t))] |= | |
| 128 | word_t (1) << (i % (CHAR_BIT * sizeof (word_t))); | |
| 129 | } | |
| 130 | ||
| 131 | /** Clear a binary digit | |
| 132 | * @param i zero-based index of the element | |
| 133 | */ | |
| 134 | void assign_false (unsigned i) { | |
| 135 | m_bits[i / (CHAR_BIT * sizeof (word_t))] &= | |
| 136 | ~(word_t (1) << (i % (CHAR_BIT * sizeof (word_t)))); | |
| 137 | } | |
| 138 | ||
| 139 | /** Determine whether the whole vector is filled with zero bits | |
| 140 | * @return 0 if all bits in the vector are clear; | |
| 141 | * index of a nonzero entry + 1 otherwise | |
| 142 | */ | |
| 143 | unsigned nonzero () const { | |
| 144 | if (!m_size) | |
| 145 | return 0; | |
| 146 | return findNext (0); | |
| 147 | } | |
| 148 | ||
| 149 | /** Find the next index at which there is a set bit | |
| 150 | * @param i the starting index (counting forward) | |
| 151 | * @return 0 if all following bits in the vector are clear; | |
| 152 | * index of the next nonzero entry + 1 otherwise | |
| 153 | */ | |
| 154 | unsigned findNext (unsigned i) const { | |
| 155 | if (i >= m_size) | |
| 156 | return 0; | |
| 157 | ||
| 158 | register const word_t* w = &m_bits[i / (CHAR_BIT * sizeof (word_t))]; | |
| 159 | register word_t bit = 1 << (i % (CHAR_BIT * sizeof (word_t))); | |
| 160 | ||
| 161 | if (*w >= bit) { | |
| 162 | // found in the same word | |
| 163 | do | |
| 164 | if (*w & bit) | |
| 165 | return i + 1; | |
| 166 | while (i++, bit <<= 1); | |
| 167 | } | |
| 168 | ||
| 169 | const word_t* const w_end = m_bits + getNumWords (m_size); | |
| 170 | ||
| 171 | // search in the remaining words | |
| 172 | while (++w < w_end) { | |
| 173 | if (!*w) continue; | |
| 174 | for (i = 1, bit = 1; !(*w & bit); bit <<= 1, i++); | |
| 175 | return i + (w - m_bits) * CHAR_BIT * sizeof (word_t); | |
| 176 | } | |
| 177 | ||
| 178 | return 0; | |
| 179 | } | |
| 180 | ||
| 181 | private: | |
| 182 | /** Number of elements in the vector */ | |
| 183 | unsigned m_size; | |
| 184 | /** Size of the allocated vector in words */ | |
| 185 | unsigned m_allocated; | |
| 186 | /** The vector */ | |
| 187 | word_t* m_bits; | |
| 188 | }; | |
| 189 | ||
| 190 | #endif // BITVECTOR_H_ |
| 0 | # Doxygen configuration file for lbt, much like a -*- makefile -*- | |
| 1 | PROJECT_NAME = LBT | |
| 2 | WARNINGS = YES | |
| 3 | HAVE_DOT = YES | |
| 4 | GRAPHICAL_HIERARCHY = YES | |
| 5 | CLASS_GRAPH = YES | |
| 6 | COLLABORATION_GRAPH = YES | |
| 7 | INCLUDE_GRAPH = YES | |
| 8 | INCLUDED_BY_GRAPH = YES | |
| 9 | INPUT = . | |
| 10 | FILE_PATTERNS = *.C *.h | |
| 11 | INCLUDE_PATH = | |
| 12 | ENABLE_PREPROCESSING = NO | |
| 13 | MACRO_EXPANSION = NO | |
| 14 | EXPAND_ONLY_PREDEF = YES | |
| 15 | SEARCH_INCLUDES = NO | |
| 16 | FULL_PATH_NAMES = NO | |
| 17 | ||
| 18 | GENERATE_LATEX = NO | |
| 19 | COMPACT_LATEX = YES | |
| 20 | PDF_HYPERLINKS = YES | |
| 21 | PAPER_TYPE = a4 | |
| 22 | ||
| 23 | GENERATE_RTF = NO | |
| 24 | GENERATE_MAN = NO | |
| 25 | ||
| 26 | GENERATE_HTML = YES | |
| 27 | SEARCHENGINE = YES | |
| 28 | CGI_NAME = lbt | |
| 29 | CGI_URL = http://siphon.tcs.hut.fi/cgi-bin | |
| 30 | DOC_URL = http://siphon.tcs.hut.fi/lbt | |
| 31 | DOC_ABSPATH = /var/www/lbt | |
| 32 | BIN_ABSPATH = /usr/lib/cgi-bin |
| 0 | // -*- c++ -*- | |
| 1 | /// @file Ltl.C | |
| 2 | /* | |
| 3 | * This file is based on code originally written by Mauno Rönkkö, | |
| 4 | * Copyright © 1998 Mauno Rönkkö <mronkko@abo.fi>. | |
| 5 | * | |
| 6 | * Modifications by Heikki Tauriainen <Heikki.Tauriainen@hut.fi> | |
| 7 | * and Marko Mäkelä <Marko.Makela@hut.fi>. | |
| 8 | * | |
| 9 | * This program is free software; you can redistribute it and/or modify | |
| 10 | * it under the terms of the GNU General Public License as published by | |
| 11 | * the Free Software Foundation; either version 2 of the License, or | |
| 12 | * (at your option) any later version. | |
| 13 | * | |
| 14 | * This program is distributed in the hope that it will be useful, | |
| 15 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
| 16 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
| 17 | * GNU General Public License for more details. | |
| 18 | * | |
| 19 | * You should have received a copy of the GNU General Public License | |
| 20 | * along with this program; if not, write to the Free Software | |
| 21 | * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. | |
| 22 | */ | |
| 23 | ||
| 24 | #ifdef __GNUC__ | |
| 25 | # pragma implementation | |
| 26 | #endif // __GNUC__ | |
| 27 | #include "Ltl.h" | |
| 28 | #include "LtlGraph.h" | |
| 29 | #include <assert.h> | |
| 30 | ||
| 31 | Ltl::Store Ltl::m_store; | |
| 32 | ||
| 33 | class Ltl& | |
| 34 | Ltl::Store::insert (class Ltl& ltl) | |
| 35 | { | |
| 36 | std::pair<std::set<class Ltl*,struct ltless>::iterator,bool> p = | |
| 37 | m_set.insert (<l); | |
| 38 | if (!p.second) | |
| 39 | delete <l; | |
| 40 | else { | |
| 41 | // new formula: add it to the translation table | |
| 42 | unsigned num = m_set.size (); | |
| 43 | if (!(num & (num - 1))) { | |
| 44 | const class Ltl** table = new const class Ltl*[num << 1]; | |
| 45 | memcpy (table, m_table, (num - 1) * sizeof *m_table); | |
| 46 | delete[] m_table; | |
| 47 | m_table = table; | |
| 48 | } | |
| 49 | m_table[ltl.m_num = num - 1] = <l; | |
| 50 | } | |
| 51 | return **p.first; | |
| 52 | } | |
| 53 | ||
| 54 | bool | |
| 55 | Ltl::operator< (const class Ltl& other) const | |
| 56 | { | |
| 57 | if (getKind () < other.getKind ()) return true; | |
| 58 | if (other.getKind () < getKind ()) return false; | |
| 59 | switch (getKind ()) { | |
| 60 | case Atom: | |
| 61 | return static_cast<const class LtlAtom&>(*this) < | |
| 62 | static_cast<const class LtlAtom&>(other); | |
| 63 | case Constant: | |
| 64 | return static_cast<const class LtlConstant&>(*this) < | |
| 65 | static_cast<const class LtlConstant&>(other); | |
| 66 | case Junct: | |
| 67 | return static_cast<const class LtlJunct&>(*this) < | |
| 68 | static_cast<const class LtlJunct&>(other); | |
| 69 | case Iff: | |
| 70 | return static_cast<const class LtlIff&>(*this) < | |
| 71 | static_cast<const class LtlIff&>(other); | |
| 72 | case Future: | |
| 73 | return static_cast<const class LtlFuture&>(*this) < | |
| 74 | static_cast<const class LtlFuture&>(other); | |
| 75 | case Until: | |
| 76 | return static_cast<const class LtlUntil&>(*this) < | |
| 77 | static_cast<const class LtlUntil&>(other); | |
| 78 | } | |
| 79 | assert (false); | |
| 80 | return false; | |
| 81 | } | |
| 82 | ||
| 83 | void | |
| 84 | LtlAtom::expand (unsigned state, | |
| 85 | class LtlGraphNode& node, | |
| 86 | class LtlGraph& graph) const | |
| 87 | { | |
| 88 | if (!node.m_old[negClone ().m_num]) { | |
| 89 | node.m_atomic.assign_true (m_num); | |
| 90 | graph.expand (state, node); | |
| 91 | } | |
| 92 | else | |
| 93 | delete &node; | |
| 94 | } | |
| 95 | ||
| 96 | void | |
| 97 | LtlConstant::expand (unsigned state, | |
| 98 | class LtlGraphNode& node, | |
| 99 | class LtlGraph& graph) const | |
| 100 | { | |
| 101 | if (!m_true) { | |
| 102 | delete &node; | |
| 103 | return; | |
| 104 | } | |
| 105 | graph.expand (state, node); | |
| 106 | } | |
| 107 | ||
| 108 | void | |
| 109 | LtlJunct::expand (unsigned state, | |
| 110 | class LtlGraphNode& node, | |
| 111 | class LtlGraph& graph) const | |
| 112 | { | |
| 113 | if (m_con) { | |
| 114 | if (!node.m_old[m_left.m_num]) | |
| 115 | node.m_new.assign_true (m_left.m_num); | |
| 116 | if (!node.m_old[m_right.m_num]) | |
| 117 | node.m_new.assign_true (m_right.m_num); | |
| 118 | } | |
| 119 | else { | |
| 120 | class BitVector new_set (node.m_new); | |
| 121 | if (!node.m_old[m_left.m_num]) | |
| 122 | new_set.assign_true (m_left.m_num); | |
| 123 | if (!node.m_old[m_right.m_num]) | |
| 124 | node.m_new.assign_true (m_right.m_num); | |
| 125 | graph.add (*new class LtlGraphNode (node.m_incoming, new_set, node.m_old, | |
| 126 | node.m_atomic, node.m_next)); | |
| 127 | } | |
| 128 | graph.expand (state, node); | |
| 129 | } | |
| 130 | ||
| 131 | void | |
| 132 | LtlIff::expand (unsigned state, | |
| 133 | class LtlGraphNode& node, | |
| 134 | class LtlGraph& graph) const | |
| 135 | { | |
| 136 | class BitVector new_set (node.m_new); | |
| 137 | class Ltl& neg_left = m_left.negClone (); | |
| 138 | class Ltl& neg_right = m_right.negClone (); | |
| 139 | if (!node.m_old[m_left.m_num]) | |
| 140 | node.m_new.assign_true (m_left.m_num); | |
| 141 | if (!new_set[neg_left.m_num]) | |
| 142 | new_set.assign_true (neg_left.m_num); | |
| 143 | if (m_iff) { | |
| 144 | if (!node.m_old[m_right.m_num]) | |
| 145 | node.m_new.assign_true (m_right.m_num); | |
| 146 | if (!new_set[neg_right.m_num]) | |
| 147 | new_set.assign_true (neg_right.m_num); | |
| 148 | } | |
| 149 | else { | |
| 150 | if (!node.m_old[neg_right.m_num]) | |
| 151 | node.m_new.assign_true (neg_right.m_num); | |
| 152 | if (!new_set[m_right.m_num]) | |
| 153 | new_set.assign_true (m_right.m_num); | |
| 154 | } | |
| 155 | graph.add (*new class LtlGraphNode (node.m_incoming, new_set, node.m_old, | |
| 156 | node.m_atomic, node.m_next)); | |
| 157 | graph.expand (state, node); | |
| 158 | } | |
| 159 | ||
| 160 | void | |
| 161 | LtlUntil::expand (unsigned state, | |
| 162 | class LtlGraphNode& node, | |
| 163 | class LtlGraph& graph) const | |
| 164 | { | |
| 165 | if (m_release) { | |
| 166 | if (!node.m_old[m_right.m_num]) | |
| 167 | node.m_new.assign_true (m_right.m_num); | |
| 168 | class BitVector new_set (node.m_new); | |
| 169 | if (!node.m_old[m_left.m_num]) | |
| 170 | node.m_new.assign_true (m_left.m_num); | |
| 171 | class BitVector next_set (node.m_next); | |
| 172 | next_set.assign_true (m_num); | |
| 173 | graph.add (*new class LtlGraphNode (node.m_incoming, new_set, node.m_old, | |
| 174 | node.m_atomic, next_set)); | |
| 175 | } | |
| 176 | else { | |
| 177 | class BitVector new_set (node.m_new); | |
| 178 | if (!node.m_old[m_left.m_num]) | |
| 179 | new_set.assign_true (m_left.m_num); | |
| 180 | if (!node.m_old[m_right.m_num]) | |
| 181 | node.m_new.assign_true (m_right.m_num); | |
| 182 | class BitVector next_set (node.m_next); | |
| 183 | next_set.assign_true (m_num); | |
| 184 | graph.add (*new class LtlGraphNode (node.m_incoming, new_set, node.m_old, | |
| 185 | node.m_atomic, next_set)); | |
| 186 | } | |
| 187 | graph.expand (state, node); | |
| 188 | } | |
| 189 | ||
| 190 | void | |
| 191 | LtlFuture::expand (unsigned state, | |
| 192 | class LtlGraphNode& node, | |
| 193 | class LtlGraph& graph) const | |
| 194 | { | |
| 195 | switch (m_op) { | |
| 196 | case next: | |
| 197 | node.m_next.assign_true (m_formula.m_num); | |
| 198 | graph.expand (state, node); | |
| 199 | return; | |
| 200 | case finally: | |
| 201 | { | |
| 202 | class BitVector new_set (node.m_new); | |
| 203 | if (!node.m_old[m_formula.m_num]) | |
| 204 | new_set.assign_true (m_formula.m_num); | |
| 205 | graph.add (*new class LtlGraphNode (node.m_incoming, | |
| 206 | new_set, | |
| 207 | node.m_old, | |
| 208 | node.m_atomic, | |
| 209 | node.m_next)); | |
| 210 | } | |
| 211 | break; | |
| 212 | case globally: | |
| 213 | if (!node.m_old[m_formula.m_num]) | |
| 214 | node.m_new.assign_true (m_formula.m_num); | |
| 215 | break; | |
| 216 | #ifndef NDEBUG | |
| 217 | default: | |
| 218 | assert (false); | |
| 219 | #endif // NDEBUG | |
| 220 | } | |
| 221 | node.m_next.assign_true (m_num); | |
| 222 | graph.expand (state, node); | |
| 223 | } |
| 0 | // -*- c++ -*- | |
| 1 | /// @file Ltl.h | |
| 2 | /* | |
| 3 | * This file is based on code originally written by Mauno Rönkkö, | |
| 4 | * Copyright © 1998 Mauno Rönkkö <mronkko@abo.fi>. | |
| 5 | * | |
| 6 | * Modifications by Heikki Tauriainen <Heikki.Tauriainen@hut.fi> | |
| 7 | * and Marko Mäkelä <Marko.Makela@hut.fi>. | |
| 8 | * | |
| 9 | * This program is free software; you can redistribute it and/or modify | |
| 10 | * it under the terms of the GNU General Public License as published by | |
| 11 | * the Free Software Foundation; either version 2 of the License, or | |
| 12 | * (at your option) any later version. | |
| 13 | * | |
| 14 | * This program is distributed in the hope that it will be useful, | |
| 15 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
| 16 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
| 17 | * GNU General Public License for more details. | |
| 18 | * | |
| 19 | * You should have received a copy of the GNU General Public License | |
| 20 | * along with this program; if not, write to the Free Software | |
| 21 | * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. | |
| 22 | */ | |
| 23 | ||
| 24 | #ifndef Ltl_h_ | |
| 25 | # define Ltl_h_ | |
| 26 | # ifdef __GNUC__ | |
| 27 | # pragma interface | |
| 28 | # endif // __GNUC__ | |
| 29 | ||
| 30 | # ifdef DEBUG | |
| 31 | # include <stdio.h> | |
| 32 | # endif // DEBUG | |
| 33 | # include <set> | |
| 34 | ||
| 35 | /** Abstract base class for LTL formulae */ | |
| 36 | class Ltl | |
| 37 | { | |
| 38 | public: | |
| 39 | /// LTL formula comparator | |
| 40 | struct ltless { | |
| 41 | /// Lexicographic order of LTL formulae | |
| 42 | /// @param l1 pointer to first formula to compare | |
| 43 | /// @param l2 pointer to second formula to compare | |
| 44 | /// @return true if l1 is before l2 | |
| 45 | bool operator() (const class Ltl* l1, | |
| 46 | const class Ltl* l2) const { | |
| 47 | return *l1 < *l2; | |
| 48 | } | |
| 49 | }; | |
| 50 | private: | |
| 51 | /// Set of instantiated LTL formulae | |
| 52 | class Store { | |
| 53 | private: | |
| 54 | /// Set of LTL formulae | |
| 55 | std::set<class Ltl*,struct ltless> m_set; | |
| 56 | /// Table of LTL formulae, indexed by Ltl::m_num | |
| 57 | const class Ltl** m_table; | |
| 58 | /// Copy constructor | |
| 59 | Store (const class Store&); | |
| 60 | /// Assignment operator | |
| 61 | class Store& operator= (const class Store&); | |
| 62 | public: | |
| 63 | /// Constructor | |
| 64 | Store () : m_set (), m_table (0) {} | |
| 65 | /// Destructor | |
| 66 | ~Store () { | |
| 67 | delete[] m_table; | |
| 68 | for (std::set<class Ltl*,struct ltless>::iterator i = m_set.begin (); | |
| 69 | i != m_set.end (); i++) { | |
| 70 | delete *i; | |
| 71 | } | |
| 72 | } | |
| 73 | /// Insert a formula to the set | |
| 74 | class Ltl& insert (class Ltl& ltl); | |
| 75 | /// Translate a formula index to a formula reference | |
| 76 | /// @param f formula index to be translated | |
| 77 | /// @return the corresponding formula | |
| 78 | const class Ltl& fetch (unsigned f) const { return *m_table[f]; } | |
| 79 | }; | |
| 80 | static class Store m_store; | |
| 81 | friend class Store; | |
| 82 | public: | |
| 83 | /// Number of the LTL formula | |
| 84 | unsigned m_num; | |
| 85 | /// Constructor | |
| 86 | Ltl () : m_num (0) {} | |
| 87 | private: | |
| 88 | /// Copy constructor | |
| 89 | Ltl (const class Ltl& old); | |
| 90 | /// Assignment operator | |
| 91 | class Ltl& operator= (const class Ltl& old); | |
| 92 | protected: | |
| 93 | /// Destructor | |
| 94 | virtual ~Ltl () {} | |
| 95 | /// Reference registrator | |
| 96 | /// @param ltl formula to be registered | |
| 97 | /// @return an equivalent formula | |
| 98 | static class Ltl& insert (class Ltl& ltl) { return m_store.insert (ltl); } | |
| 99 | public: | |
| 100 | /// Translate a formula index to a formula reference | |
| 101 | /// @param f formula index to be translated | |
| 102 | /// @return the corresponding formula | |
| 103 | static const class Ltl& fetch (unsigned f) { return m_store.fetch (f); } | |
| 104 | ||
| 105 | /// Returns a clone of the negation of this Ltl formula. | |
| 106 | virtual class Ltl& negClone () const = 0; | |
| 107 | ||
| 108 | /// Formula kinds | |
| 109 | enum Kind { Atom, Constant, Junct, Iff, Future, Until }; | |
| 110 | /// Determine the kind of the formula | |
| 111 | virtual enum Kind getKind () const = 0; | |
| 112 | /// Less-than comparison | |
| 113 | bool operator< (const class Ltl& other) const; | |
| 114 | ||
| 115 | /// Implements operator/operand specific details of the expansion algorithm. | |
| 116 | /// @param state state number in the generalized Büchi automaton | |
| 117 | /// @param node the node representing the formula | |
| 118 | /// @param graph graph representation of the generalized Büchi automaton | |
| 119 | virtual void expand (unsigned state, | |
| 120 | class LtlGraphNode& node, | |
| 121 | class LtlGraph& graph) const = 0; | |
| 122 | ||
| 123 | # ifdef DEBUG | |
| 124 | /// Stream output | |
| 125 | virtual void display (FILE* out) const = 0; | |
| 126 | # endif // DEBUG | |
| 127 | }; | |
| 128 | ||
| 129 | /** LTL atom */ | |
| 130 | class LtlAtom : public Ltl | |
| 131 | { | |
| 132 | private: | |
| 133 | /// The proposition number | |
| 134 | unsigned m_value; | |
| 135 | /// Flag: is the proposition negated? | |
| 136 | bool m_negated; | |
| 137 | ||
| 138 | public: | |
| 139 | /// Constructor | |
| 140 | /// @param value proposition number | |
| 141 | /// @param negated flag: is the proposition negated? | |
| 142 | /// @return an LTL atom | |
| 143 | static class Ltl& construct (unsigned value, bool negated) { | |
| 144 | return insert (*new class LtlAtom (value, negated)); | |
| 145 | } | |
| 146 | /// Returns a clone of the negation of this Ltl formula. | |
| 147 | class Ltl& negClone () const { | |
| 148 | return insert (*new class LtlAtom (m_value, !m_negated)); | |
| 149 | } | |
| 150 | private: | |
| 151 | /// Constructor | |
| 152 | LtlAtom (unsigned value, bool negated = false) : | |
| 153 | Ltl (), m_value (value), m_negated (negated) {} | |
| 154 | /// Copy constructor | |
| 155 | LtlAtom (const class LtlAtom& old); | |
| 156 | /// Assignment operator | |
| 157 | class LtlAtom& operator= (const class LtlAtom& old); | |
| 158 | protected: | |
| 159 | /// Destructor | |
| 160 | ~LtlAtom () {} | |
| 161 | public: | |
| 162 | ||
| 163 | /// Determine the kind of the formula | |
| 164 | enum Kind getKind () const { return Atom; } | |
| 165 | /// Less-than comparison | |
| 166 | bool operator< (const class LtlAtom& other) const { | |
| 167 | return m_value < other.m_value || | |
| 168 | (m_value == other.m_value && m_negated < other.m_negated); | |
| 169 | } | |
| 170 | ||
| 171 | /// Determine whether the atom is negated | |
| 172 | bool isNegated () const { return m_negated; } | |
| 173 | /// Determine the value of the proposition | |
| 174 | unsigned getValue () const { return m_value; } | |
| 175 | ||
| 176 | /// Implements operator/operand specific details of the expansion algorithm. | |
| 177 | /// @param state state number in the generalized Büchi automaton | |
| 178 | /// @param node the node representing the formula | |
| 179 | /// @param graph graph representation of the generalized Büchi automaton | |
| 180 | void expand (unsigned state, | |
| 181 | class LtlGraphNode& node, | |
| 182 | class LtlGraph& graph) const; | |
| 183 | ||
| 184 | # ifdef DEBUG | |
| 185 | /// Stream output | |
| 186 | void display (FILE* out) const { | |
| 187 | if (m_negated) fputs ("! ", out); | |
| 188 | fprintf (out, "p%u", m_value); | |
| 189 | } | |
| 190 | # endif // DEBUG | |
| 191 | }; | |
| 192 | ||
| 193 | /** LTL constants 'true' and 'false' */ | |
| 194 | class LtlConstant : public Ltl | |
| 195 | { | |
| 196 | private: | |
| 197 | /// The truth value of the constant | |
| 198 | bool m_true; | |
| 199 | ||
| 200 | public: | |
| 201 | /// Constructor | |
| 202 | /// @param true_ the constant 'true' or 'false' | |
| 203 | /// @return an LTL constant | |
| 204 | static class Ltl& construct (bool true_) { | |
| 205 | return insert (*new class LtlConstant (true_)); | |
| 206 | } | |
| 207 | /// Returns a clone of the negation of this Ltl formula. | |
| 208 | class Ltl& negClone () const { | |
| 209 | return insert (*new class LtlConstant (!m_true)); | |
| 210 | } | |
| 211 | private: | |
| 212 | /// Constructor | |
| 213 | LtlConstant (bool true_) : Ltl (), m_true (true_) {} | |
| 214 | /// Copy constructor | |
| 215 | LtlConstant (const class LtlConstant& old); | |
| 216 | /// Assignment operator | |
| 217 | class LtlConstant& operator= (const class LtlConstant& old); | |
| 218 | protected: | |
| 219 | /// Destructor | |
| 220 | ~LtlConstant () {} | |
| 221 | public: | |
| 222 | ||
| 223 | /// Determine the kind of the formula | |
| 224 | enum Kind getKind () const { return Constant; } | |
| 225 | /// Less-than comparison | |
| 226 | bool operator< (const class LtlConstant& other) const { | |
| 227 | return m_true < other.m_true; | |
| 228 | } | |
| 229 | ||
| 230 | /// Convert to truth value | |
| 231 | operator bool () const { return m_true; } | |
| 232 | ||
| 233 | /// Implements operator/operand specific details of the expansion algorithm. | |
| 234 | /// @param state state number in the generalized Büchi automaton | |
| 235 | /// @param node the node representing the formula | |
| 236 | /// @param graph graph representation of the generalized Büchi automaton | |
| 237 | void expand (unsigned state, | |
| 238 | class LtlGraphNode& node, | |
| 239 | class LtlGraph& graph) const; | |
| 240 | ||
| 241 | # ifdef DEBUG | |
| 242 | /// Stream output | |
| 243 | void display (FILE* out) const { putc (m_true ? 't' : 'f', out); } | |
| 244 | # endif // DEBUG | |
| 245 | }; | |
| 246 | ||
| 247 | /** LTL conjunction and disjunction */ | |
| 248 | class LtlJunct : public Ltl | |
| 249 | { | |
| 250 | private: | |
| 251 | /// Flag: conjunction instead of disjunction? | |
| 252 | bool m_con; | |
| 253 | /// The left-hand-side sub-formula | |
| 254 | class Ltl& m_left; | |
| 255 | /// The right-hand-side sub-formula | |
| 256 | class Ltl& m_right; | |
| 257 | ||
| 258 | public: | |
| 259 | /// Optimizing constructor | |
| 260 | /// @param con flag: conjunction instead of disjunction | |
| 261 | /// @param l the left-hand-side formula | |
| 262 | /// @param r the right-hand-side formula | |
| 263 | /// @return an equivalent formula | |
| 264 | static class Ltl& construct (bool con, | |
| 265 | class Ltl& l, | |
| 266 | class Ltl& r) { | |
| 267 | if (l.getKind () == Ltl::Constant) | |
| 268 | return bool (static_cast<class LtlConstant&>(l)) == con ? r : l; | |
| 269 | if (r.getKind () == Ltl::Constant) | |
| 270 | return bool (static_cast<class LtlConstant&>(r)) == con ? l : r; | |
| 271 | if (&l == &r) | |
| 272 | return l; | |
| 273 | return &l < &r | |
| 274 | ? insert (*new class LtlJunct (con, l, r)) | |
| 275 | : insert (*new class LtlJunct (con, r, l)); | |
| 276 | } | |
| 277 | /// Returns a clone of the negation of this Ltl formula. | |
| 278 | class Ltl& negClone () const { | |
| 279 | return insert (*new class LtlJunct (!m_con, | |
| 280 | m_left.negClone (), | |
| 281 | m_right.negClone ())); | |
| 282 | } | |
| 283 | ||
| 284 | private: | |
| 285 | /// Constructor | |
| 286 | /// @param con flag: conjunction instead of disjunction | |
| 287 | /// @param l the left-hand-side formula | |
| 288 | /// @param r the right-hand-side formula | |
| 289 | LtlJunct (bool con, | |
| 290 | class Ltl& l, | |
| 291 | class Ltl& r) : | |
| 292 | m_con (con), m_left (l), m_right (r) {} | |
| 293 | /// Copy constructor | |
| 294 | LtlJunct (const class LtlJunct& old); | |
| 295 | /// Assignment operator | |
| 296 | class LtlJunct& operator= (const class LtlJunct& old); | |
| 297 | protected: | |
| 298 | /// Destructor | |
| 299 | ~LtlJunct () {} | |
| 300 | public: | |
| 301 | ||
| 302 | /// Determine the kind of the formula | |
| 303 | enum Kind getKind () const { return Junct; } | |
| 304 | /// Less-than comparison | |
| 305 | bool operator< (const class LtlJunct& other) const { | |
| 306 | if (m_con < other.m_con) return true; | |
| 307 | if (other.m_con < m_con) return false; | |
| 308 | if (&m_left < &other.m_left) return true; | |
| 309 | if (&other.m_left < &m_left) return false; | |
| 310 | return &m_right < &other.m_right; | |
| 311 | } | |
| 312 | ||
| 313 | /// Implements operator/operand specific details of the expansion algorithm. | |
| 314 | /// @param state state number in the generalized Büchi automaton | |
| 315 | /// @param node the node representing the formula | |
| 316 | /// @param graph graph representation of the generalized Büchi automaton | |
| 317 | void expand (unsigned state, | |
| 318 | class LtlGraphNode& node, | |
| 319 | class LtlGraph& graph) const; | |
| 320 | ||
| 321 | # ifdef DEBUG | |
| 322 | /// Stream output | |
| 323 | void display (FILE* out) const { | |
| 324 | fputs (m_con ? "& " : "| ", out); | |
| 325 | m_left.display (out); | |
| 326 | putc (' ', out); | |
| 327 | m_right.display (out); | |
| 328 | } | |
| 329 | # endif // DEBUG | |
| 330 | }; | |
| 331 | ||
| 332 | /** LTL equivalence or exclusive disjunction */ | |
| 333 | class LtlIff : public Ltl | |
| 334 | { | |
| 335 | private: | |
| 336 | /// Flag: equivalence instead of exclusive disjunction? | |
| 337 | bool m_iff; | |
| 338 | /// The left-hand-side sub-formula | |
| 339 | class Ltl& m_left; | |
| 340 | /// The right-hand-side sub-formula | |
| 341 | class Ltl& m_right; | |
| 342 | ||
| 343 | public: | |
| 344 | /// Optimizing constructor | |
| 345 | /// @param iff flag: equivalence instead of exclusive disjunction | |
| 346 | /// @param l the left-hand-side formula | |
| 347 | /// @param r the right-hand-side formula | |
| 348 | /// @return an equivalent formula | |
| 349 | static class Ltl& construct (bool iff, | |
| 350 | class Ltl& l, | |
| 351 | class Ltl& r) { | |
| 352 | if (l.getKind () == Ltl::Constant) | |
| 353 | return bool (static_cast<class LtlConstant&>(l)) == iff | |
| 354 | ? r | |
| 355 | : r.negClone (); | |
| 356 | if (r.getKind () == Ltl::Constant) | |
| 357 | return bool (static_cast<class LtlConstant&>(r)) == iff | |
| 358 | ? l | |
| 359 | : l.negClone (); | |
| 360 | if (&l == &r) | |
| 361 | return LtlConstant::construct (iff); | |
| 362 | return &l < &r | |
| 363 | ? insert (*new class LtlIff (iff, l, r)) | |
| 364 | : insert (*new class LtlIff (iff, r, l)); | |
| 365 | } | |
| 366 | /// Returns a clone of the negation of this Ltl formula. | |
| 367 | class Ltl& negClone () const { | |
| 368 | return insert (*new class LtlIff (!m_iff, | |
| 369 | m_left, | |
| 370 | m_right)); | |
| 371 | } | |
| 372 | ||
| 373 | private: | |
| 374 | /// Constructor | |
| 375 | /// @param iff flag: equivalence instead of exclusive disjunction | |
| 376 | /// @param l the left-hand-side formula | |
| 377 | /// @param r the right-hand-side formula | |
| 378 | LtlIff (bool iff, | |
| 379 | class Ltl& l, | |
| 380 | class Ltl& r) : | |
| 381 | m_iff (iff), m_left (l), m_right (r) {} | |
| 382 | /// Copy constructor | |
| 383 | LtlIff (const class LtlIff& old); | |
| 384 | /// Assignment operator | |
| 385 | class LtlIff& operator= (const class LtlIff& old); | |
| 386 | protected: | |
| 387 | /// Destructor | |
| 388 | ~LtlIff () {} | |
| 389 | public: | |
| 390 | ||
| 391 | /// Determine the kind of the formula | |
| 392 | enum Kind getKind () const {return Iff; } | |
| 393 | /// Less-than comparison | |
| 394 | bool operator< (const class LtlIff& other) const { | |
| 395 | if (m_iff < other.m_iff) return true; | |
| 396 | if (other.m_iff < m_iff) return false; | |
| 397 | if (&m_left < &other.m_left) return true; | |
| 398 | if (&other.m_left < &m_left) return false; | |
| 399 | return &m_right < &other.m_right; | |
| 400 | } | |
| 401 | ||
| 402 | /// Implements operator/operand specific details of the expansion algorithm. | |
| 403 | /// @param state state number in the generalized Büchi automaton | |
| 404 | /// @param node the node representing the formula | |
| 405 | /// @param graph graph representation of the generalized Büchi automaton | |
| 406 | void expand (unsigned state, | |
| 407 | class LtlGraphNode& node, | |
| 408 | class LtlGraph& graph) const; | |
| 409 | ||
| 410 | # ifdef DEBUG | |
| 411 | /// Stream output | |
| 412 | void display (FILE* out) const { | |
| 413 | fputs (m_iff ? "e " : "^ ", out); | |
| 414 | m_left.display (out); | |
| 415 | putc (' ', out); | |
| 416 | m_right.display (out); | |
| 417 | } | |
| 418 | # endif // DEBUG | |
| 419 | }; | |
| 420 | ||
| 421 | /** LTL next-time, globally and finally formulae */ | |
| 422 | class LtlFuture : public Ltl | |
| 423 | { | |
| 424 | public: | |
| 425 | /// Operator kinds | |
| 426 | enum Op { next, globally, finally }; | |
| 427 | private: | |
| 428 | /// The operator | |
| 429 | enum Op m_op; | |
| 430 | /// The formula being quantified | |
| 431 | class Ltl& m_formula; | |
| 432 | ||
| 433 | public: | |
| 434 | /// Constructor | |
| 435 | /// @param op the operator | |
| 436 | /// @param f the formula | |
| 437 | /// @return an LTL future formula | |
| 438 | static class Ltl& construct (enum Op op, | |
| 439 | class Ltl& f) { | |
| 440 | return insert (*new class LtlFuture (op, f)); | |
| 441 | } | |
| 442 | /// Returns a clone of the negation of this formula. | |
| 443 | class Ltl& negClone () const { | |
| 444 | switch (m_op) { | |
| 445 | case next: | |
| 446 | break; | |
| 447 | case globally: | |
| 448 | return insert (*new class LtlFuture (finally, m_formula.negClone ())); | |
| 449 | case finally: | |
| 450 | return insert (*new class LtlFuture (globally, m_formula.negClone ())); | |
| 451 | } | |
| 452 | return insert (*new class LtlFuture (m_op, m_formula.negClone ())); | |
| 453 | } | |
| 454 | ||
| 455 | private: | |
| 456 | /// Constructor | |
| 457 | /// @param op the operator | |
| 458 | /// @param f the formula | |
| 459 | /// @param r the right-hand-side formula | |
| 460 | LtlFuture (enum Op op, | |
| 461 | class Ltl& f) : | |
| 462 | m_op (op), m_formula (f) {} | |
| 463 | /// Copy constructor | |
| 464 | LtlFuture (const class LtlFuture& old); | |
| 465 | /// Assignment operator | |
| 466 | class LtlFuture& operator= (const class LtlFuture& old); | |
| 467 | protected: | |
| 468 | /// Destructor | |
| 469 | ~LtlFuture () {} | |
| 470 | public: | |
| 471 | ||
| 472 | /// Determine the kind of the formula | |
| 473 | enum Kind getKind () const { return Future; } | |
| 474 | /// Less-than comparison | |
| 475 | bool operator< (const class LtlFuture& other) const { | |
| 476 | if (m_op < other.m_op) return true; | |
| 477 | if (other.m_op < m_op) return false; | |
| 478 | return &m_formula < &other.m_formula; | |
| 479 | } | |
| 480 | ||
| 481 | /// Get the temporal operator | |
| 482 | enum Op getOp () const { return m_op; } | |
| 483 | /// Get the subformula | |
| 484 | const class Ltl& getFormula () const { return m_formula; } | |
| 485 | ||
| 486 | /// Implements operator/operand specific details of the expansion algorithm. | |
| 487 | /// @param state state number in the generalized Büchi automaton | |
| 488 | /// @param node the node representing the formula | |
| 489 | /// @param graph graph representation of the generalized Büchi automaton | |
| 490 | void expand (unsigned state, | |
| 491 | class LtlGraphNode& node, | |
| 492 | class LtlGraph& graph) const; | |
| 493 | ||
| 494 | # ifdef DEBUG | |
| 495 | /// Stream output | |
| 496 | void display (FILE* out) const { | |
| 497 | switch (m_op) { | |
| 498 | case next: | |
| 499 | putc ('X', out); break; | |
| 500 | case globally: | |
| 501 | putc ('G', out); break; | |
| 502 | case finally: | |
| 503 | putc ('F', out); break; | |
| 504 | } | |
| 505 | putc (' ', out); | |
| 506 | m_formula.display (out); | |
| 507 | } | |
| 508 | # endif // DEBUG | |
| 509 | }; | |
| 510 | ||
| 511 | /** LTL 'until' and 'release' operators */ | |
| 512 | class LtlUntil : public Ltl | |
| 513 | { | |
| 514 | private: | |
| 515 | /// Flag: release instead of until | |
| 516 | bool m_release; | |
| 517 | /// The left-hand-side sub-formula | |
| 518 | class Ltl& m_left; | |
| 519 | /// The right-hand-side sub-formula | |
| 520 | class Ltl& m_right; | |
| 521 | ||
| 522 | public: | |
| 523 | /// Constructor | |
| 524 | /// @param release flag: 'release' instead of 'until' | |
| 525 | /// @param l the left-hand-side formula | |
| 526 | /// @param r the right-hand-side formula | |
| 527 | /// @return an LTL formula | |
| 528 | static class Ltl& construct (bool release, | |
| 529 | class Ltl& l, | |
| 530 | class Ltl& r) { | |
| 531 | return insert (*new class LtlUntil (release, l, r)); | |
| 532 | } | |
| 533 | private: | |
| 534 | /// Constructor | |
| 535 | /// @param release flag: 'release' instead of 'until' | |
| 536 | /// @param l the left-hand-side formula | |
| 537 | /// @param r the right-hand-side formula | |
| 538 | LtlUntil (bool release, | |
| 539 | class Ltl& l, | |
| 540 | class Ltl& r) : | |
| 541 | m_release (release), m_left (l), m_right (r) {} | |
| 542 | /// Copy constructor | |
| 543 | LtlUntil (const class LtlUntil& old); | |
| 544 | /// Assignment operator | |
| 545 | class LtlUntil& operator= (const class LtlUntil& old); | |
| 546 | public: | |
| 547 | /// Destructor | |
| 548 | ~LtlUntil () {} | |
| 549 | ||
| 550 | /// Returns a clone of the negation of this Ltl formula. | |
| 551 | class Ltl& negClone () const { | |
| 552 | return insert (*new class LtlUntil (!m_release, | |
| 553 | m_left.negClone (), | |
| 554 | m_right.negClone ())); | |
| 555 | } | |
| 556 | ||
| 557 | /// Determine the kind of the formula | |
| 558 | enum Kind getKind () const { return Until; } | |
| 559 | /// Less-than comparison | |
| 560 | bool operator< (const class LtlUntil& other) const { | |
| 561 | if (m_release < other.m_release) return true; | |
| 562 | if (other.m_release < m_release) return false; | |
| 563 | if (&m_left < &other.m_left) return true; | |
| 564 | if (&other.m_left < &m_left) return false; | |
| 565 | return &m_right < &other.m_right; | |
| 566 | } | |
| 567 | ||
| 568 | /// Determine whether this is a release operator instead of until | |
| 569 | bool isRelease () const { return m_release; } | |
| 570 | /// Get the left-hand-side subformula | |
| 571 | const class Ltl& getLeft () const { return m_left; } | |
| 572 | /// Get the right-hand-side subformula | |
| 573 | const class Ltl& getRight () const { return m_right; } | |
| 574 | ||
| 575 | /// Implements operator/operand specific details of the expansion algorithm. | |
| 576 | /// @param state state number in the generalized Büchi automaton | |
| 577 | /// @param node the node representing the formula | |
| 578 | /// @param graph graph representation of the generalized Büchi automaton | |
| 579 | void expand (unsigned state, | |
| 580 | class LtlGraphNode& node, | |
| 581 | class LtlGraph& graph) const; | |
| 582 | ||
| 583 | # ifdef DEBUG | |
| 584 | /// Stream output | |
| 585 | void display (FILE* out) const { | |
| 586 | fputs (m_release ? "V " : "U ", out); | |
| 587 | m_left.display (out); | |
| 588 | putc (' ', out); | |
| 589 | m_right.display (out); | |
| 590 | } | |
| 591 | # endif // DEBUG | |
| 592 | }; | |
| 593 | ||
| 594 | #endif // Ltl_h_ |
| 0 | // -*- c++ -*- | |
| 1 | /// @file LtlGraph.C | |
| 2 | /* | |
| 3 | * This file is based on code originally written by Mauno Rönkkö, | |
| 4 | * Copyright © 1998 Mauno Rönkkö <mronkko@abo.fi>. | |
| 5 | * | |
| 6 | * Modifications by Heikki Tauriainen <Heikki.Tauriainen@hut.fi> | |
| 7 | * and Marko Mäkelä <Marko.Makela@hut.fi>. | |
| 8 | * | |
| 9 | * This program is free software; you can redistribute it and/or modify | |
| 10 | * it under the terms of the GNU General Public License as published by | |
| 11 | * the Free Software Foundation; either version 2 of the License, or | |
| 12 | * (at your option) any later version. | |
| 13 | * | |
| 14 | * This program is distributed in the hope that it will be useful, | |
| 15 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
| 16 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
| 17 | * GNU General Public License for more details. | |
| 18 | * | |
| 19 | * You should have received a copy of the GNU General Public License | |
| 20 | * along with this program; if not, write to the Free Software | |
| 21 | * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. | |
| 22 | */ | |
| 23 | ||
| 24 | #ifdef __GNUC__ | |
| 25 | # pragma implementation | |
| 26 | #endif // __GNUC__ | |
| 27 | #include "LtlGraph.h" | |
| 28 | ||
| 29 | /// An empty formula set | |
| 30 | static const class BitVector e; | |
| 31 | ||
| 32 | LtlGraph::LtlGraph (const class Ltl& formula) : | |
| 33 | m_next (1), m_nodes () | |
| 34 | { | |
| 35 | std::set<unsigned> incoming; | |
| 36 | incoming.insert (0); | |
| 37 | ||
| 38 | class BitVector new_set (formula.m_num + 1); | |
| 39 | new_set.assign_true (formula.m_num); | |
| 40 | ||
| 41 | expand (1, *new class LtlGraphNode (incoming, new_set, e, e, e)); | |
| 42 | } | |
| 43 | ||
| 44 | void | |
| 45 | LtlGraph::expand (unsigned state, | |
| 46 | class LtlGraphNode& node) | |
| 47 | { | |
| 48 | if (unsigned p = node.m_new.nonzero ()) { | |
| 49 | p--; | |
| 50 | node.m_old.assign_true (p); | |
| 51 | node.m_new.assign_false (p); | |
| 52 | Ltl::fetch (p).expand (state, node, *this); | |
| 53 | return; | |
| 54 | } | |
| 55 | ||
| 56 | // no new propositions: merge the node with the graph | |
| 57 | // search for an existing node having the same 'old' and 'next' sets | |
| 58 | for (iterator i = m_nodes.begin (); i != m_nodes.end (); i++) { | |
| 59 | if (i->second.m_old == node.m_old && i->second.m_next == node.m_next) { | |
| 60 | // merge the node with an existing one | |
| 61 | for (std::set<unsigned>::const_iterator j = node.m_incoming.begin (); | |
| 62 | j != node.m_incoming.end(); j++) | |
| 63 | i->second.m_incoming.insert (*j); | |
| 64 | delete &node; | |
| 65 | return; | |
| 66 | } | |
| 67 | } | |
| 68 | ||
| 69 | // a genuinely new node: insert it to the graph and expand further | |
| 70 | m_nodes.insert (std::pair<unsigned,class LtlGraphNode> (m_next, node)); | |
| 71 | std::set<unsigned> incoming; | |
| 72 | incoming.insert (m_next++); | |
| 73 | class LtlGraphNode* node2 = | |
| 74 | new class LtlGraphNode (incoming, node.m_next, e, e, e); | |
| 75 | delete &node; | |
| 76 | expand (m_next, *node2); | |
| 77 | } |
| 0 | // -*- c++ -*- | |
| 1 | /// @file LtlGraph.h | |
| 2 | /* | |
| 3 | * This file is based on code originally written by Mauno Rönkkö, | |
| 4 | * Copyright © 1998 Mauno Rönkkö <mronkko@abo.fi>. | |
| 5 | * | |
| 6 | * Modifications by Heikki Tauriainen <Heikki.Tauriainen@hut.fi> | |
| 7 | * and Marko Mäkelä <Marko.Makela@hut.fi>. | |
| 8 | * | |
| 9 | * This program is free software; you can redistribute it and/or modify | |
| 10 | * it under the terms of the GNU General Public License as published by | |
| 11 | * the Free Software Foundation; either version 2 of the License, or | |
| 12 | * (at your option) any later version. | |
| 13 | * | |
| 14 | * This program is distributed in the hope that it will be useful, | |
| 15 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
| 16 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
| 17 | * GNU General Public License for more details. | |
| 18 | * | |
| 19 | * You should have received a copy of the GNU General Public License | |
| 20 | * along with this program; if not, write to the Free Software | |
| 21 | * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA. | |
| 22 | */ | |
| 23 | ||
| 24 | #ifndef LtlGraph_h_ | |
| 25 | # define LtlGraph_h_ | |
| 26 | # ifdef __GNUC__ | |
| 27 | # pragma interface | |
| 28 | # endif // __GNUC__ | |
| 29 | ||
| 30 | # include "Ltl.h" | |
| 31 | # include "BitVector.h" | |
| 32 | # include <map> | |
| 33 | ||
| 34 | /** | |
| 35 | * A node in a graph representing an LTL formula. | |
| 36 | * | |
| 37 | * The graph itself is a set of nodes of this kind. | |
| 38 | * The LtlGraphNode class is merely a front end for the set representation. | |
| 39 | */ | |
| 40 | class LtlGraphNode | |
| 41 | { | |
| 42 | public: | |
| 43 | /// From which nodes can one come to this node. | |
| 44 | std::set<unsigned> m_incoming; | |
| 45 | /// A set of formulae to be processed. | |
| 46 | class BitVector m_new; | |
| 47 | /// A set of formulae that must hold, when this node is entered. | |
| 48 | class BitVector m_old; | |
| 49 | /// A set of atomic propositions that must hold, when this node is entered. | |
| 50 | class BitVector m_atomic; | |
| 51 | /// A set of formulae that must hold in immediate next nodes. | |
| 52 | class BitVector m_next; | |
| 53 | ||
| 54 | /// Default constructor | |
| 55 | LtlGraphNode () : | |
| 56 | m_incoming (), m_new (), m_old (), m_atomic (), m_next () {} | |
| 57 | ||
| 58 | /// Constructs a specific node. | |
| 59 | LtlGraphNode (const std::set<unsigned>& incoming, | |
| 60 | const class BitVector& neww, | |
| 61 | const class BitVector& old, | |
| 62 | const class BitVector& atomic, | |
| 63 | const class BitVector& next) : | |
| 64 | m_incoming (incoming), m_new (neww), m_old (old), | |
| 65 | m_atomic (atomic), m_next (next) {} | |
| 66 | /// Copy constructor | |
| 67 | LtlGraphNode (const class LtlGraphNode& node) : | |
| 68 | m_incoming (node.m_incoming), m_new (node.m_new), | |
| 69 | m_old (node.m_old), m_atomic (node.m_atomic), m_next (node.m_next) {} | |
| 70 | private: | |
| 71 | /// Assignment operator | |
| 72 | class LtlGraphNode& operator= (const class LtlGraphNode& node); | |
| 73 | public: | |
| 74 | /// Destructor | |
| 75 | ~LtlGraphNode () {} | |
| 76 | }; | |
| 77 | ||
| 78 | /** | |
| 79 | * Graph representation of a generalized Büchi automaton | |
| 80 | * corresponding to an LTL formula | |
| 81 | * | |
| 82 | * A LtlGraph is automatically constructed from a given | |
| 83 | * Ltl formula. All relevant information is fully stored to the | |
| 84 | * graph, so that the formula itself may well be destoyed right after | |
| 85 | * the conversion. The Ltl operators/operands provide themselves | |
| 86 | * the knowledge of how to be expanded into a LtlGraph. | |
| 87 | */ | |
| 88 | class LtlGraph | |
| 89 | { | |
| 90 | public: | |
| 91 | /*@{*/ | |
| 92 | /// Map from state numbers to graph nodes | |
| 93 | typedef std::map<unsigned,class LtlGraphNode> Map; | |
| 94 | /// Iterator to the map | |
| 95 | typedef Map::iterator iterator; | |
| 96 | /// Constant iterator to the map | |
| 97 | typedef Map::const_iterator const_iterator; | |
| 98 | /*@}*/ | |
| 99 | private: | |
| 100 | /// Next available state number | |
| 101 | unsigned m_next; | |
| 102 | ||
| 103 | /// Map from state numbers to graph nodes (0=initial state) | |
| 104 | std::map<unsigned,class LtlGraphNode> m_nodes; | |
| 105 | ||
| 106 | public: | |
| 107 | /// Expand an LTL subformula into the graph | |
| 108 | /// @param state state number in the automaton | |
| 109 | /// @param node the node representing the LTL subformula | |
| 110 | void expand (unsigned state, | |
| 111 | class LtlGraphNode& node); | |
| 112 | /// Expand an LTL subformula into the graph | |
| 113 | /// @param node the node representing a new LTL subformula | |
| 114 | void add (class LtlGraphNode& node) { expand (m_next++, node); } | |
| 115 | ||
| 116 | private: | |
| 117 | /// Copy constructor | |
| 118 | LtlGraph (const class LtlGraph& old); | |
| 119 | /// Assignment operator | |
| 120 | class LtlGraph& operator= (const class LtlGraph& other); | |
| 121 | public: | |
| 122 | /// Constructs a graph from a given LTL formula. | |
| 123 | LtlGraph (const class Ltl& formula); | |
| 124 | ||
| 125 | /// Destructor | |
| 126 | ~LtlGraph () {} | |
| 127 | ||
| 128 | /** @name Accessors to the graph nodes */ | |
| 129 | /*@{*/ | |
| 130 | const_iterator begin () const { return m_nodes.begin (); } | |
| 131 | const_iterator end () const { return m_nodes.end (); } | |
| 132 | /*@}*/ | |
| 133 | }; | |
| 134 | ||
| 135 | #endif // LtlGraph_h_ |
| 0 | # Installation directory prefix for Debian GNU/Linux | |
| 1 | DESTDIR = | |
| 2 | # Generic installation directory prefix | |
| 3 | PREFIX = $(DESTDIR)/usr | |
| 4 | ||
| 5 | # Where to put binaries on 'make install'? | |
| 6 | BINDIR = $(PREFIX)/bin | |
| 7 | # Where to put documentation on 'make install'? | |
| 8 | DOCDIR = $(PREFIX)/share/doc/lbt | |
| 9 | # Where to put manual pages on 'make installman'? | |
| 10 | MANDIR = $(PREFIX)/share/man/man1 | |
| 11 | ||
| 12 | # Installation commands | |
| 13 | INSTALLDIR = install -d | |
| 14 | INSTALLBIN = install | |
| 15 | INSTALLDATA = install -m 444 | |
| 16 | RM = rm -f | |
| 17 | ||
| 18 | # GCC (tested with 2.95.4 and 3.0.2) | |
| 19 | CXX=g++ | |
| 20 | CXXFLAGS=$(CFLAGS) -fno-exceptions -fno-rtti | |
| 21 | LDFLAGS= | |
| 22 | CC=gcc | |
| 23 | CFLAGS=-O3 | |
| 24 | ||
| 25 | ## Compaq C++ V6.3-011 for Digital UNIX V4.0G (Rev. 1530) | |
| 26 | #CXX=cxx | |
| 27 | #CXXFLAGS=$(CFLAGS) -nocleanup -nortti | |
| 28 | #LDFLAGS= | |
| 29 | #CC=cc | |
| 30 | #CFLAGS=-arch host -tune host -assume trusted_short_alignment -assume noptrs_to_globals -compress -O5 -w1 -std strict_ansi_errors | |
| 31 | ||
| 32 | TARGETS = lbt lbt2dot | |
| 33 | LBTOBJS = Ltl.o LtlGraph.o BitVector.o lbt.o | |
| 34 | L2DOBJS = lbt2dot.o | |
| 35 | ||
| 36 | OBJS = $(LBTOBJS) $(L2DOBJS) | |
| 37 | ||
| 38 | MANPAGES = lbt.1 lbt2dot.1 | |
| 39 | ||
| 40 | all: $(TARGETS) | |
| 41 | ||
| 42 | clean: | |
| 43 | $(RM) $(OBJS) | |
| 44 | reallyclean: clean | |
| 45 | $(RM) $(TARGETS) | |
| 46 | ||
| 47 | install: $(TARGETS) | |
| 48 | $(INSTALLDIR) $(BINDIR) $(DOCDIR) | |
| 49 | $(INSTALLBIN) lbt lbt2dot $(BINDIR) | |
| 50 | $(INSTALLDATA) doc/* $(DOCDIR) | |
| 51 | ||
| 52 | installman: $(MANPAGES) | |
| 53 | $(INSTALLDIR) $(MANDIR) | |
| 54 | $(INSTALLDATA) $(MANPAGES) $(MANDIR) | |
| 55 | ||
| 56 | lbt: $(LBTOBJS) | |
| 57 | $(CXX) -o $@ $(LBTOBJS) $(LDFLAGS) | |
| 58 | lbt2dot: $(L2DOBJS) | |
| 59 | $(CC) -o $@ $(L2DOBJS) $(LDFLAGS) | |
| 60 | ||
| 61 | .C.o: | |
| 62 | $(CXX) $(CXXFLAGS) -c $< -o $@ | |
| 63 | .c.o: | |
| 64 | $(CC) $(CFLAGS) -c $< -o $@ | |
| 65 | ||
| 66 | .phony: all clean reallyclean install installman | |
| 67 | .SUFFIXES: | |
| 68 | .SUFFIXES: .C .c .o | |
| 69 | ||
| 70 | Ltl.o LtlGraph.o lbt.o: Ltl.h LtlGraph.h BitVector.h | |
| 71 | BitVector.o: BitVector.h |
| 0 | 2002-04-19 Marko =?ISO-8859-1?Q?M=E4kel=E4?= <Marko.Makela@HUT.FI> | |
| 1 | ||
| 2 | lbt 1.2.1 was released. | |
| 3 | ||
| 4 | * NEWS: Described these changes. | |
| 5 | * notgp0.png, notgp0-opt.png: Rendered with anti-aliased fonts. | |
| 6 | * index.html: Corrected a few minor errors in the grammar, | |
| 7 | and updated the address of Mauno Rönkkö. | |
| 8 | ||
| 9 | 2001-10-03 Marko Mäkelä <Marko.Makela@HUT.FI> | |
| 10 | ||
| 11 | lbt 1.2 was released. | |
| 12 | ||
| 13 | * NEWS: Initial revision | |
| 14 | * BitVector.h, BitVector.C: Initial revision | |
| 15 | * Makefile: Added a few variable definitions | |
| 16 |
| 0 | LBT NEWS -- history of user-visible changes. 23rd April 2002 | |
| 1 | Copyright © 2001,2002 Marko Mäkelä | |
| 2 | See the end for copying conditions. | |
| 3 | ||
| 4 | * LBT 1.2.1 improves the documentation only | |
| 5 | ||
| 6 | ** A few minor errors were corrected in the grammar description. | |
| 7 | ||
| 8 | ** The pictures of the automata were redrawn with anti-aliased fonts. | |
| 9 | ||
| 10 | * LBT 1.2 is an optimized release with no user-visible changes | |
| 11 | ||
| 12 | ** Formula sets are now maintained in bit vectors | |
| 13 | instead of Standard Template Library sets. This typically reduces | |
| 14 | the memory usage and improves the speed of the program. The generated | |
| 15 | automata should be of the same size as with LBT 1.1, but the acceptance | |
| 16 | sets for the states can be displayed in a slightly different order. | |
| 17 | ||
| 18 | * New operators in LBT 1.1 | |
| 19 | ||
| 20 | ** The equivalence and nonequivalence (exclusive or) operators are supported | |
| 21 | natively by the translation algorithm of LBT 1.1. When these operators are | |
| 22 | implemented in the core language, formulae that contain these operators can | |
| 23 | be expressed in a much more compact way. | |
| 24 | ||
| 25 | * LBT 1.0 | |
| 26 | ||
| 27 | ** A complete rewrite of the algorithms from Mauno Rönkkö's LBT2BUCHI | |
| 28 | and Heikki Tauriainen's super_aasa_lbt. | |
| 29 | ||
| 30 | ** Common subformula elimination reduces the size of the generated automata. | |
| 31 | ||
| 32 | ||
| 33 | ---------------------------------------------------------------------- | |
| 34 | Copyright information: | |
| 35 | ||
| 36 | Copyright © 2001,2002 Marko Mäkelä | |
| 37 | ||
| 38 | Permission is granted to anyone to make or distribute verbatim copies | |
| 39 | of this document as received, in any medium, provided that the | |
| 40 | copyright notice and this permission notice are preserved, | |
| 41 | thus giving the recipient permission to redistribute in turn. | |
| 42 | ||
| 43 | Permission is granted to distribute modified versions | |
| 44 | of this document, or of portions of it, | |
| 45 | under the above conditions, provided also that they | |
| 46 | carry prominent notices stating who last changed them. | |
| 47 | ||
| 48 | Local variables: | |
| 49 | mode: outline | |
| 50 | paragraph-separate: "[ ]*$" | |
| 51 | end: |
| 0 | <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0//EN"> | |
| 1 | ||
| 2 | <HTML><HEAD> | |
| 3 | <TITLE>LBT: LTL to Büchi converter</TITLE> | |
| 4 | <LINK REV=MADE HREF="mailto:msmakela@tcs.hut.fi"> | |
| 5 | </HEAD> | |
| 6 | <BODY> | |
| 7 | ||
| 8 | <H1>LBT: LTL to Büchi conversion</H1> | |
| 9 | ||
| 10 | <P>This piece of software provides a C++ implementation for an | |
| 11 | algorithm that converts a linear temporal logic formula to a | |
| 12 | generalised Büchi automaton. The algorithm comes from</P> | |
| 13 | ||
| 14 | <BLOCKQUOTE><P>R. Gerth, D. Peled, Y. Vardi, and | |
| 15 | <A HREF="http://www.montefiore.ulg.ac.be/%7Epw/">P. Wolper</A>. | |
| 16 | <BR> | |
| 17 | <EM><A HREF="http://www.montefiore.ulg.ac.be/%7Epw/papers/psfiles/GPVW95.ps">Simple on-the-fly automatic verification of linear temporal logic.</A></EM> | |
| 18 | PSTV'95, Fifteenth International Symposium on PROTOCOL SPECIFICATION, TESTING AND VERIFICATION, Warsaw, Poland, 1995.</P></BLOCKQUOTE> | |
| 19 | ||
| 20 | <P>The resulting automaton may be used, for instance, in model | |
| 21 | checking, where it represents a property to be verified from a model | |
| 22 | (e.g. a Petri net).</P> | |
| 23 | ||
| 24 | <H2>Copyright</H2> | |
| 25 | ||
| 26 | <P>The implementation is Copyright © 1999 <A | |
| 27 | HREF="http://staff.cs.utu.fi/%7Emronkko/PROJECT/LTL2BUCHI/abstract.html">Mauno | |
| 28 | Rönkkö</A> <mauno.ronkko@cs.utu.fi>. The original copyright | |
| 29 | statement follows:</P> | |
| 30 | ||
| 31 | <BLOCKQUOTE><P>This product contains free software; you can | |
| 32 | redistribute it and/or modify it under the terms of the <A | |
| 33 | HREF="http://www.fsf.org/copyleft/gpl.html">GNU General Public | |
| 34 | License</A> as published by the <A HREF="http://www.fsf.org/">Free | |
| 35 | Software Foundation</A>; either version 2 of the License, or (at your | |
| 36 | option) any later version. These terms also apply to any hardware | |
| 37 | schemas and any other information presented in the www-pages | |
| 38 | below.</P> | |
| 39 | ||
| 40 | <P>This product information is distributed in the hope that it will | |
| 41 | be useful, but WITHOUT ANY WARRANTY; without even the implied warranty | |
| 42 | of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. This also | |
| 43 | applies to any hardware schemas and any other information described in | |
| 44 | the www-pages below. See the GNU General Public License for more | |
| 45 | details. You should be able to read the GNU General Public License | |
| 46 | via the above link; if not, write to the Free Software Foundation, | |
| 47 | Inc., 675 Mass Ave, Cambridge, MA 02139, USA.</P></BLOCKQUOTE> | |
| 48 | ||
| 49 | <P>Enhancements and packaging are © 1999-2001 Heikki Tauriainen | |
| 50 | <heikki.tauriainen@hut.fi>, and © 2001 Marko Mäkelä | |
| 51 | <marko.makela@hut.fi>.</P> | |
| 52 | ||
| 53 | <H1>Interfacing the Translator</H1> | |
| 54 | ||
| 55 | <P>The translator is designed to be invoked as a subprocess. It | |
| 56 | parses a linear temporal logic from standard input and writes a | |
| 57 | corresponding generalised Büchi automaton to standard output, and | |
| 58 | exits. Both the input and output format are based on prefix notation | |
| 59 | that facilitate straightforward recursive-descent parsing.</P> | |
| 60 | ||
| 61 | <H2>Grammar Definitions</H2> | |
| 62 | ||
| 63 | <P>The grammar is presented in Backus-Naur Form, one grammar rule per | |
| 64 | line. Comments delimited by the symbols <EM>/*</EM> and <EM>*/</EM> | |
| 65 | are not part of the formal grammar. Non-terminal symbols are enclosed | |
| 66 | within single quotes or presented as <A | |
| 67 | HREF="http://www.gnu.org/software/flex/flex.html">Flex</A>-style | |
| 68 | regular-expressions.</P> | |
| 69 | ||
| 70 | <H3>Input format for LTL formulae</H3> | |
| 71 | ||
| 72 | <H4>Propositional operators</H4> | |
| 73 | ||
| 74 | <TABLE> | |
| 75 | <TR> | |
| 76 | <TD><A NAME="f"><f></A> ::=</TD> | |
| 77 | <TD><CODE>'t'</CODE></TD> | |
| 78 | <TD><EM>/* true */</EM></TD> | |
| 79 | </TR> | |
| 80 | <TR> | |
| 81 | <TD><f> ::=</TD> | |
| 82 | <TD><CODE>'f'</CODE></TD> | |
| 83 | <TD><EM>/* false */</EM></TD> | |
| 84 | </TR> | |
| 85 | <TR> | |
| 86 | <TD><f> ::=</TD> | |
| 87 | <TD><CODE>'p'[0-9]+</CODE></TD> | |
| 88 | <TD><EM>/* proposition */</EM></TD> | |
| 89 | </TR> | |
| 90 | <TR> | |
| 91 | <TD><f> ::=</TD> | |
| 92 | <TD><CODE>'!'</CODE> | |
| 93 | <<A HREF="#f">f</A>></TD> | |
| 94 | <TD><EM>/* negation */</EM></TD> | |
| 95 | </TR> | |
| 96 | <TR> | |
| 97 | <TD><f> ::=</TD> | |
| 98 | <TD><CODE>'|'</CODE> | |
| 99 | <<A HREF="#f">f</A>> | |
| 100 | <<A HREF="#f">f</A>></TD> | |
| 101 | <TD><EM>/* disjunction */</EM></TD> | |
| 102 | </TR> | |
| 103 | <TR> | |
| 104 | <TD><f> ::=</TD> | |
| 105 | <TD><CODE>'&'</CODE> | |
| 106 | <<A HREF="#f">f</A>> | |
| 107 | <<A HREF="#f">f</A>></TD> | |
| 108 | <TD><EM>/* conjunction */</EM></TD> | |
| 109 | </TR> | |
| 110 | <TR> | |
| 111 | <TD><f> ::=</TD> | |
| 112 | <TD><CODE>'i'</CODE> | |
| 113 | <<A HREF="#f">f</A>> | |
| 114 | <<A HREF="#f">f</A>></TD> | |
| 115 | <TD><EM>/* implication: | |
| 116 | <CODE>"i <f1> <f2>"</CODE> is short-hand for | |
| 117 | <CODE>"| ! <f1> <f2>"</CODE> */</EM></TD> | |
| 118 | </TR> | |
| 119 | <TR> | |
| 120 | <TD><f> ::=</TD> | |
| 121 | <TD><CODE>'e'</CODE> | |
| 122 | <<A HREF="#f">f</A>> | |
| 123 | <<A HREF="#f">f</A>></TD> | |
| 124 | <TD><EM>/* equivalence */</EM></TD> | |
| 125 | </TR> | |
| 126 | <TR> | |
| 127 | <TD><f> ::=</TD> | |
| 128 | <TD><CODE>'^'</CODE> | |
| 129 | <<A HREF="#f">f</A>> | |
| 130 | <<A HREF="#f">f</A>></TD> | |
| 131 | <TD><EM>/* exclusive disjunction (xor) */</EM></TD> | |
| 132 | </TR> | |
| 133 | <TR> | |
| 134 | <TD><f> ::=</TD> | |
| 135 | <TD><CODE>[ \t\n\r\v\f]</CODE> <<A HREF="#f">f</A>></TD> | |
| 136 | <TD><EM>/* white space is ignored */</EM></TD> | |
| 137 | </TR> | |
| 138 | <TR> | |
| 139 | <TD><f> ::=</TD> | |
| 140 | <TD><<A HREF="#f">f</A>> <CODE>[ \t\n\r\v\f]</CODE></TD> | |
| 141 | <TD><EM>/* white space is ignored */</EM></TD> | |
| 142 | </TR> | |
| 143 | </TABLE> | |
| 144 | ||
| 145 | <H4>Temporal operators</H4> | |
| 146 | ||
| 147 | <TABLE> | |
| 148 | <TR> | |
| 149 | <TD><f> ::=</TD> | |
| 150 | <TD><CODE>'X'</CODE> | |
| 151 | <<A HREF="#f">f</A>></TD> | |
| 152 | <TD><EM>/* next */</EM></TD> | |
| 153 | </TR> | |
| 154 | <TR> | |
| 155 | <TD><f> ::=</TD> | |
| 156 | <TD><CODE>'F'</CODE> | |
| 157 | <<A HREF="#f">f</A>></TD> | |
| 158 | <TD><EM>/* finally, eventually */</EM></TD> | |
| 159 | </TR> | |
| 160 | <TR> | |
| 161 | <TD><f> ::=</TD> | |
| 162 | <TD><CODE>'G'</CODE> | |
| 163 | <<A HREF="#f">f</A>></TD> | |
| 164 | <TD><EM>/* globally, henceforth */</EM></TD> | |
| 165 | </TR> | |
| 166 | <TR> | |
| 167 | <TD><f> ::=</TD> | |
| 168 | <TD><CODE>'U'</CODE> | |
| 169 | <<A HREF="#f">f</A>> | |
| 170 | <<A HREF="#f">f</A>></TD> | |
| 171 | <TD><EM>/* until */</EM></TD> | |
| 172 | </TR> | |
| 173 | <TR> | |
| 174 | <TD><f> ::=</TD> | |
| 175 | <TD><CODE>'V'</CODE> | |
| 176 | <<A HREF="#f">f</A>> | |
| 177 | <<A HREF="#f">f</A>></TD> | |
| 178 | <TD><EM>/* release */</EM></TD> | |
| 179 | </TR> | |
| 180 | </TABLE> | |
| 181 | ||
| 182 | <H2>Output format for generalised Büchi automata</H2> | |
| 183 | ||
| 184 | <TABLE> | |
| 185 | <TR> | |
| 186 | <TD><A NAME="space"><space></A> ::=</TD> | |
| 187 | <TD><CODE>[ \n]+</CODE></TD> | |
| 188 | </TR> | |
| 189 | <TR> | |
| 190 | <TD><A NAME="gba"><gba></A> ::=</TD> | |
| 191 | <TD><CODE>[0-9]+</CODE> <<A HREF="#space">space</A>> | |
| 192 | <CODE>[0-9]+</CODE> | |
| 193 | <<A HREF="#states">states</A>> | |
| 194 | </TD> | |
| 195 | <TD><EM>/* first the number of states, then the number of acceptance sets | |
| 196 | (if 0, all states are accepting) */</EM></TD> | |
| 197 | </TR> | |
| 198 | <TR> | |
| 199 | <TD><A NAME="states"><states></A> ::=</TD> | |
| 200 | <TD><EM>/* empty */</EM></TD> | |
| 201 | </TR> | |
| 202 | <TR> | |
| 203 | <TD><states> ::=</TD> | |
| 204 | <TD><<A HREF="#states">states</A>> <<A HREF="#space">space</A>> | |
| 205 | <<A HREF="#state">state</A>></TD> | |
| 206 | </TR> | |
| 207 | <TR> | |
| 208 | <TD><A NAME="state"><state></A> ::=</TD> | |
| 209 | <TD><CODE>[0-9]+</CODE> <<A HREF="#space">space</A>> | |
| 210 | <<A HREF="#initial">initial?</A>> <<A HREF="#space">space</A>> | |
| 211 | <<A HREF="#acceptance sets">acceptance sets</A>> '-1' | |
| 212 | <<A HREF="#transitions">transitions</A>> '-1'</TD> | |
| 213 | <TD><EM>/* state identifiers can be arbitrary unsigned integers */</EM></TD> | |
| 214 | </TR> | |
| 215 | <TR> | |
| 216 | <TD><A NAME="initial"><initial?></A> ::=</TD> | |
| 217 | <TD><CODE>'0'</CODE></TD> | |
| 218 | <TD><EM>/* not an initial state */</EM></TD> | |
| 219 | </TR> | |
| 220 | <TR> | |
| 221 | <TD><initial?> ::=</TD> | |
| 222 | <TD><CODE>'1'</CODE></TD> | |
| 223 | <TD><EM>/* initial state (exactly one state must be initial) */</EM></TD> | |
| 224 | </TR> | |
| 225 | <TR> | |
| 226 | <TD><A NAME="acceptance sets"><acceptance sets></A> ::=</TD> | |
| 227 | <TD><EM>/* empty */</EM></TD> | |
| 228 | </TR> | |
| 229 | <TR> | |
| 230 | <TD><acceptance sets> ::=</TD> | |
| 231 | <TD><<A HREF="#acceptance sets">acceptance sets</A>> | |
| 232 | <CODE>[0-9]+</CODE> <<A HREF="#space">space</A>></TD> | |
| 233 | <TD><EM>/* acceptance set identifiers can be arbitrary unsigned integers */</EM></TD> | |
| 234 | </TR> | |
| 235 | <TR> | |
| 236 | <TD><A NAME="transitions"><transitions></A> ::=</TD> | |
| 237 | <TD><EM>/* empty */</EM></TD> | |
| 238 | </TR> | |
| 239 | <TR> | |
| 240 | <TD><transitions> ::=</TD> | |
| 241 | <TD><<A HREF="#transitions">transitions</A>> | |
| 242 | <<A HREF="#space">space</A>> | |
| 243 | <<A HREF="#transition">transition</A>></TD> | |
| 244 | </TR> | |
| 245 | <TR> | |
| 246 | <TD><A NAME="transition"><transition></A> ::=</TD> | |
| 247 | <TD><CODE>[0-9]+</CODE> <<A HREF="#space">space</A>> | |
| 248 | <CODE>'t'</CODE></TD> | |
| 249 | <TD><EM>/* constantly enabled transition to | |
| 250 | a <A HREF="#state">state</A> */</EM></TD> | |
| 251 | </TR> | |
| 252 | <TR> | |
| 253 | <TD><A NAME="transition"><transition></A> ::=</TD> | |
| 254 | <TD><CODE>[0-9]+</CODE> <<A HREF="#space">space</A>> | |
| 255 | <<A HREF="#gate">gate</A>></TD> | |
| 256 | <TD><EM>/* conditionally enabled transition to | |
| 257 | a <A HREF="#state">state</A> */</EM></TD> | |
| 258 | </TR> | |
| 259 | <TR> | |
| 260 | <TD><A NAME="gate"><gate></A> ::=</TD> | |
| 261 | <TD><CODE>'p'[0-9]+</CODE></TD> | |
| 262 | <TD><EM>/* proposition */</EM></TD> | |
| 263 | </TR> | |
| 264 | <TR> | |
| 265 | <TD><gate> ::=</TD> | |
| 266 | <TD><CODE>'!'</CODE> <<A HREF="#space">space</A>> | |
| 267 | <<A HREF="#gate">gate</A>></TD> | |
| 268 | <TD><EM>/* negation */</EM></TD> | |
| 269 | </TR> | |
| 270 | <TR> | |
| 271 | <TD><gate> ::=</TD> | |
| 272 | <TD><CODE>'|'</CODE> <<A HREF="#space">space</A>> | |
| 273 | <<A HREF="#gate">gate</A>> <<A HREF="#space">space</A>> | |
| 274 | <<A HREF="#gate">gate</A>></TD> | |
| 275 | <TD><EM>/* disjunction */</EM></TD> | |
| 276 | </TR> | |
| 277 | <TR> | |
| 278 | <TD><gate> ::=</TD> | |
| 279 | <TD><CODE>'&'</CODE> <<A HREF="#space">space</A>> | |
| 280 | <<A HREF="#gate">gate</A>> <<A HREF="#space">space</A>> | |
| 281 | <<A HREF="#gate">gate</A>></TD> | |
| 282 | <TD><EM>/* conjunction */</EM></TD> | |
| 283 | </TR> | |
| 284 | </TABLE> | |
| 285 | ||
| 286 | <P>Note that currently LBT does not generate disjunctions on gate | |
| 287 | conditions. Also, the initial state is always numbered 0.</P> | |
| 288 | ||
| 289 | <H2>Visualising the Output</H2> | |
| 290 | ||
| 291 | <P>A simple tool, lbt2dot, converts the generalised Büchi automata | |
| 292 | descriptions output by the translator to a format viewable with <A | |
| 293 | HREF="http://www.graphviz.org/">GraphViz</A>, a visualisation tool for | |
| 294 | directed graphs. Gate expressions are presented as edge labels, and | |
| 295 | state and acceptance set identifiers are presented as node labels. | |
| 296 | The node corresponding to the initial state is shaded.</P> | |
| 297 | ||
| 298 | <P>Here is a sample run involving the filter: <CODE>echo '! G p0' | | |
| 299 | lbt | lbt2dot | dotty -</CODE>.<BR> | |
| 300 | <IMG SRC="notgp0.png" ALT="[Generalised Büchi Automaton of ! G p0]"><BR> | |
| 301 | In the picture above, constructed with the command <CODE>echo '! G p0' | |
| 302 | | lbt | lbt2dot | dot -Tpng -Grankdir=LR -Nfontname=Verdana | |
| 303 | -Efontname=Verdana > notgp0.png</CODE>, the automaton has 4 states, | |
| 304 | identified by the numbers 0, 2, 3, and 4. The initial state is 0, and | |
| 305 | there is one acceptance set, identified by the number 0. All states | |
| 306 | except states 0 and 4 belong to this acceptance set.</P> | |
| 307 | ||
| 308 | <P>The above example illustrates that the translation generates | |
| 309 | unnecessary states. The algoritm never generates loops to the initial | |
| 310 | state. Clearly, this automaton could be reduced to two states with | |
| 311 | <CODE>t</CODE>-labeled self-loops:<BR> | |
| 312 | <IMG SRC="notgp0-opt.png" ALT="[Optimised Generalised Büchi Automaton of ! G p0]"></P> | |
| 313 | ||
| 314 | <H1>Obtaining the Code</H1> | |
| 315 | ||
| 316 | <P>You can download the code from <A | |
| 317 | HREF="http://www.tcs.hut.fi/maria/src/">http://www.tcs.hut.fi/maria/src/</A>. | |
| 318 | You will need C and C++ compilers such as <A | |
| 319 | HREF="http://gcc.gnu.org/">GCC</A> for compiling the source code.</P> | |
| 320 | ||
| 321 | <P>For the convenience of Windows users, we provide executable files | |
| 322 | that were compiled with gcc-2.95.2 configured as a cross-compiler for | |
| 323 | the <A HREF="http://www.mingw.org/">mingw</A> target platform.</P> | |
| 324 | ||
| 325 | </BODY></HTML> |
Binary diff not shown
Binary diff not shown
| 0 | .\" Hey, EMACS: -*- nroff -*- | |
| 1 | .\" First parameter, NAME, should be all caps | |
| 2 | .\" Second parameter, SECTION, should be 1-8, maybe w/ subsection | |
| 3 | .\" other parameters are allowed: see man(7), man(1) | |
| 4 | .TH LBT 1 "August 10, 2001" | |
| 5 | .\" Please adjust this date whenever revising the manpage. | |
| 6 | .\" | |
| 7 | .\" Some roff macros, for reference: | |
| 8 | .\" .nh disable hyphenation | |
| 9 | .\" .hy enable hyphenation | |
| 10 | .\" .ad l left justify | |
| 11 | .\" .ad b justify to both left and right margins | |
| 12 | .\" .nf disable filling | |
| 13 | .\" .fi enable filling | |
| 14 | .\" .br insert line break | |
| 15 | .\" .sp <n> insert n+1 empty lines | |
| 16 | .\" for manpage-specific macros, see man(7) | |
| 17 | .SH NAME | |
| 18 | lbt \- LTL to B\(:uchi Translator | |
| 19 | .SH SYNOPSIS | |
| 20 | .B lbt | |
| 21 | .RI "< " formula.txt " > " automaton.txt | |
| 22 | .br | |
| 23 | .B lbt2dot | |
| 24 | .RI "< " automaton.txt " > " automaton.dot | |
| 25 | .SH DESCRIPTION | |
| 26 | This manual page documents briefly the | |
| 27 | .B lbt | |
| 28 | and | |
| 29 | .B lbt2dot | |
| 30 | commands. | |
| 31 | This manual page was written for the Debian GNU/Linux distribution | |
| 32 | because the original program does not have a manual page. | |
| 33 | Instead, it has documentation in HTML format; see below. | |
| 34 | .PP | |
| 35 | .\" TeX users may be more comfortable with the \fB<whatever>\fP and | |
| 36 | .\" \fI<whatever>\fP escape sequences to invode bold face and italics, | |
| 37 | .\" respectively. | |
| 38 | \fBlbt\fP is a filter that translates a linear temporal logic (LTL) | |
| 39 | formula to a corresponding generalized B\(:uchi automaton. The | |
| 40 | translation is based on the algorithm by Gerth, Peled and Vardi | |
| 41 | presented at PSTV'95, | |
| 42 | .IR "Simple on-the-fly automatic verification of linear temporal logic". | |
| 43 | Hardly any optimizations are implemented, and the generated automaton | |
| 44 | is often bigger than necessary. But on the other hand, it should always | |
| 45 | be correct. | |
| 46 | .br | |
| 47 | The filter \fBlbt2dot\fP can be used to translate Büchi automata from the | |
| 48 | \fBlbt\fP output format to GraphViz format for visualization. | |
| 49 | .SH EXAMPLE | |
| 50 | \fBecho\fP G p0 | \fBlbt\fP | \fBlbt2dot\fP | \fBdotty\fP - | |
| 51 | .SH SEE ALSO | |
| 52 | .BR dotty (1). | |
| 53 | .SH FILES | |
| 54 | .TP | |
| 55 | .I /usr/share/doc/lbt/html/index.html | |
| 56 | The real documentation for LBT. | |
| 57 | .SH AUTHOR | |
| 58 | This manual page was written by Marko M\(:akel\(:a <msmakela@tcs.hut.fi>, | |
| 59 | for the Debian GNU/Linux system (but may be used by others). | |
| 60 | The \fBlbt\fP program was written by | |
| 61 | .B Mauno R\(:onkk\(:o | |
| 62 | and | |
| 63 | .B Heikki Tauriainen, | |
| 64 | and it was optimized by | |
| 65 | .B Marko M\(:akel\(:a, | |
| 66 | who also wrote the \fBlbt2dot\fP filter. | |
| 67 | Please see the copyright file in | |
| 68 | .I /usr/share/doc/lbt | |
| 69 | for details. |
| 0 | /// @file lbt.C | |
| 1 | /// The main program of lbt | |
| 2 | ||
| 3 | /* | |
| 4 | * Copyright © 2001 Heikki Tauriainen <Heikki.Tauriainen@hut.fi> | |
| 5 | * Copyright © 2001 Marko Mäkelä <msmakela@tcs.hut.fi> | |
| 6 | * | |
| 7 | * This program is free software; you can redistribute it and/or | |
| 8 | * modify it under the terms of the GNU General Public License | |
| 9 | * as published by the Free Software Foundation; either version 2 | |
| 10 | * of the License, or (at your option) any later version. | |
| 11 | * | |
| 12 | * This program is distributed in the hope that it will be useful, | |
| 13 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
| 14 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
| 15 | * GNU General Public License for more details. | |
| 16 | * | |
| 17 | * You should have received a copy of the GNU General Public License | |
| 18 | * along with this program; if not, write to the Free Software | |
| 19 | * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. | |
| 20 | */ | |
| 21 | ||
| 22 | /** @mainpage LBT: LTL to Büchi Translator | |
| 23 | * @htmlonly | |
| 24 | * Please visit also the | |
| 25 | * <a href="http://www.tcs.hut.fi/maria/tools/lbt/">LBT home page</a>. | |
| 26 | * @endhtmlonly | |
| 27 | */ | |
| 28 | ||
| 29 | #include "LtlGraph.h" | |
| 30 | #include <stdio.h> | |
| 31 | ||
| 32 | /** Read an LTL formula from standard input | |
| 33 | * @param negation flag: negate the formula | |
| 34 | * @return the parsed formula, or NULL on error | |
| 35 | */ | |
| 36 | static class Ltl* | |
| 37 | readFormula (bool negation) | |
| 38 | { | |
| 39 | int ch; | |
| 40 | class Ltl *left, *right; | |
| 41 | loop: | |
| 42 | while ((ch = getchar ()) == ' ' || ch == '\n' || ch == '\r' || | |
| 43 | ch == '\t' || ch == '\v' || ch == '\f'); | |
| 44 | switch (ch) { | |
| 45 | case 't': | |
| 46 | case 'f': | |
| 47 | return &LtlConstant::construct ((ch == 'f') == negation); | |
| 48 | case 'p': | |
| 49 | if (1 == scanf ("%u", &ch)) | |
| 50 | return &LtlAtom::construct (ch, negation); | |
| 51 | fputs ("error in proposition number\n", stderr); | |
| 52 | return 0; | |
| 53 | case '!': | |
| 54 | negation = !negation; | |
| 55 | goto loop; | |
| 56 | case '&': | |
| 57 | case '|': | |
| 58 | if ((left = readFormula (negation)) && (right = readFormula (negation))) | |
| 59 | return &LtlJunct::construct ((ch == '&') != negation, *left, *right); | |
| 60 | return 0; | |
| 61 | case 'i': | |
| 62 | if ((left = readFormula (!negation)) && (right = readFormula (negation))) | |
| 63 | return &LtlJunct::construct (negation, *left, *right); | |
| 64 | return 0; | |
| 65 | case 'e': | |
| 66 | case '^' : | |
| 67 | if ((left = readFormula (false)) && (right = readFormula (false))) | |
| 68 | return &LtlIff::construct ((ch == 'e') != negation, *left, *right); | |
| 69 | return 0; | |
| 70 | case 'X': | |
| 71 | return (left = readFormula (negation)) | |
| 72 | ? &LtlFuture::construct (LtlFuture::next, *left) | |
| 73 | : 0; | |
| 74 | case 'F': | |
| 75 | case 'G': | |
| 76 | return (left = readFormula (negation)) | |
| 77 | ? &LtlFuture::construct ((ch == 'F') == negation | |
| 78 | ? LtlFuture::globally | |
| 79 | : LtlFuture::finally, *left) | |
| 80 | : 0; | |
| 81 | case 'U': | |
| 82 | case 'V': | |
| 83 | if ((left = readFormula (negation)) && (right = readFormula (negation))) | |
| 84 | return &LtlUntil::construct ((ch == 'U') == negation, *left, *right); | |
| 85 | case EOF: | |
| 86 | fputs ("unexpected end of file while parsing formula\n", stderr); | |
| 87 | return 0; | |
| 88 | default: | |
| 89 | fprintf (stderr, "unknown character 0x%02x\n", ch); | |
| 90 | return 0; | |
| 91 | } | |
| 92 | } | |
| 93 | ||
| 94 | /** Display the gates for arcs leaving a specific Büchi automaton state | |
| 95 | * @param gba the generalized Büchi automaton | |
| 96 | * @param state the state whose successor arcs are to be displayed | |
| 97 | */ | |
| 98 | static void | |
| 99 | printGates (const class LtlGraph& gba, | |
| 100 | unsigned state) | |
| 101 | { | |
| 102 | for (LtlGraph::const_iterator n = gba.begin (); n != gba.end (); n++) { | |
| 103 | if (n->second.m_incoming.find (state) == | |
| 104 | const_cast<std::set<unsigned>&>(n->second.m_incoming).end ()) | |
| 105 | continue; | |
| 106 | const class BitVector& propositions = n->second.m_atomic; | |
| 107 | printf ("%u ", n->first); | |
| 108 | /** Previously encountered gate expression */ | |
| 109 | const class LtlAtom* gate = 0; | |
| 110 | ||
| 111 | for (unsigned i = propositions.nonzero (); i; ) { | |
| 112 | if (gate) | |
| 113 | printf (gate->isNegated () ? "& ! p%u " : "& p%u ", | |
| 114 | gate->getValue ()); | |
| 115 | gate = &static_cast<const class LtlAtom&>(Ltl::fetch (i - 1)); | |
| 116 | if (i) i = propositions.findNext (i); | |
| 117 | } | |
| 118 | if (gate) | |
| 119 | printf (gate->isNegated () ? "! p%u\n" : "p%u\n", gate->getValue ()); | |
| 120 | else | |
| 121 | puts ("t"); | |
| 122 | } | |
| 123 | puts ("-1"); | |
| 124 | } | |
| 125 | ||
| 126 | /** Translate a formula and output the automaton to standard output | |
| 127 | * @param formula the formula to be translated | |
| 128 | */ | |
| 129 | static void | |
| 130 | translateFormula (const class Ltl& formula) | |
| 131 | { | |
| 132 | /** The generalized Büchi automaton */ | |
| 133 | class LtlGraph gba (formula); | |
| 134 | /** acceptance set number and proposition */ | |
| 135 | typedef std::pair<unsigned, const class Ltl*> acceptance_set_t; | |
| 136 | typedef std::map<const class Ltl*, acceptance_set_t> acceptance_map_t; | |
| 137 | acceptance_map_t acceptance_sets; | |
| 138 | ||
| 139 | /** number of states */ | |
| 140 | unsigned numStates = 0; | |
| 141 | /** iterator to states */ | |
| 142 | LtlGraph::const_iterator s; | |
| 143 | ||
| 144 | // construct the acceptance sets | |
| 145 | for (s = gba.begin (); s != gba.end (); s++) { | |
| 146 | numStates++; | |
| 147 | const class BitVector& temporal = s->second.m_old; | |
| 148 | for (unsigned i = temporal.nonzero (); i; ) { | |
| 149 | const class Ltl& f = Ltl::fetch (i - 1); | |
| 150 | switch (f.getKind ()) { | |
| 151 | case Ltl::Until: | |
| 152 | if (!static_cast<const class LtlUntil&>(f).isRelease ()) | |
| 153 | acceptance_sets.insert (std::pair<const class Ltl*,acceptance_set_t> | |
| 154 | (&f, acceptance_set_t | |
| 155 | (acceptance_sets.size (), | |
| 156 | &static_cast<const class LtlUntil&> | |
| 157 | (f).getRight ()))); | |
| 158 | break; | |
| 159 | case Ltl::Future: | |
| 160 | if (static_cast<const class LtlFuture&>(f).getOp () == | |
| 161 | LtlFuture::finally) | |
| 162 | acceptance_sets.insert (std::pair<const class Ltl*,acceptance_set_t> | |
| 163 | (&f, acceptance_set_t | |
| 164 | (acceptance_sets.size (), | |
| 165 | &static_cast<const class LtlFuture&> | |
| 166 | (f).getFormula ()))); | |
| 167 | break; | |
| 168 | default: | |
| 169 | break; | |
| 170 | } | |
| 171 | if (i) i = temporal.findNext (i); | |
| 172 | } | |
| 173 | } | |
| 174 | ||
| 175 | if (numStates) { | |
| 176 | printf ("%u %u", numStates + 1, acceptance_sets.size ()); | |
| 177 | puts ("\n0 1 -1"); | |
| 178 | printGates (gba, 0); | |
| 179 | } | |
| 180 | else | |
| 181 | puts ("0 0"); | |
| 182 | ||
| 183 | for (s = gba.begin (); s != gba.end (); s++) { | |
| 184 | printf ("%u 0", s->first); | |
| 185 | const class BitVector& temporal = s->second.m_old; | |
| 186 | ||
| 187 | // determine and display the acceptance sets the state belongs to | |
| 188 | for (acceptance_map_t::iterator a = acceptance_sets.begin (); | |
| 189 | a != acceptance_sets.end (); a++) { | |
| 190 | /** flag: does the state belong to the acceptance set? */ | |
| 191 | bool accepting = true; | |
| 192 | ||
| 193 | for (unsigned i = temporal.nonzero (); i; ) { | |
| 194 | const class Ltl* f = &Ltl::fetch (i - 1); | |
| 195 | if (f == a->second.second) { | |
| 196 | accepting = true; | |
| 197 | break; | |
| 198 | } | |
| 199 | else if (f == a->first) | |
| 200 | accepting = false; | |
| 201 | if (i) i = temporal.findNext (i); | |
| 202 | } | |
| 203 | ||
| 204 | if (accepting) | |
| 205 | printf (" %u", a->second.first); | |
| 206 | } | |
| 207 | ||
| 208 | puts (" -1"); | |
| 209 | printGates (gba, s->first); | |
| 210 | } | |
| 211 | } | |
| 212 | ||
| 213 | int main(int argc, char* argv[]) | |
| 214 | { | |
| 215 | if (argc > 1) { | |
| 216 | fputs ("usage: ", stderr); | |
| 217 | fputs (*argv, stderr); | |
| 218 | fputs (" < formula.txt > automaton.txt\n", stderr); | |
| 219 | return 1; | |
| 220 | } | |
| 221 | ||
| 222 | if (class Ltl* formula = readFormula (false)) { | |
| 223 | translateFormula (*formula); | |
| 224 | int ch; | |
| 225 | while ((ch = getchar ()) == ' ' || ch == '\n' || ch == '\r' || | |
| 226 | ch == '\t' || ch == '\v' || ch == '\f'); | |
| 227 | if (ch != EOF) { | |
| 228 | fputs ("ignoring extraneous input: '", stderr); | |
| 229 | do putc (ch, stderr); while ((ch = getchar ()) != EOF); | |
| 230 | fputs ("'\n", stderr); | |
| 231 | return 2; | |
| 232 | } | |
| 233 | } | |
| 234 | else | |
| 235 | return 2; | |
| 236 | ||
| 237 | return 0; | |
| 238 | } |
| 0 | /** | |
| 1 | * @file lbt2dot.c | |
| 2 | * This filter converts an lbt-generated automaton to a GraphViz digraph | |
| 3 | * @author Marko.Makela@hut.fi (Marko Mäkelä) | |
| 4 | */ | |
| 5 | /* | |
| 6 | * | |
| 7 | * Copyright © 2001 Marko Mäkelä <Marko.Makela@hut.fi> | |
| 8 | * | |
| 9 | * This program is free software; you can redistribute it and/or | |
| 10 | * modify it under the terms of the GNU General Public License | |
| 11 | * as published by the Free Software Foundation; either version 2 | |
| 12 | * of the License, or (at your option) any later version. | |
| 13 | * | |
| 14 | * This program is distributed in the hope that it will be useful, | |
| 15 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
| 16 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
| 17 | * GNU General Public License for more details. | |
| 18 | * | |
| 19 | * You should have received a copy of the GNU General Public License | |
| 20 | * along with this program; if not, write to the Free Software | |
| 21 | * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. | |
| 22 | */ | |
| 23 | #include<ctype.h> | |
| 24 | #include<stdio.h> | |
| 25 | #include<limits.h> | |
| 26 | ||
| 27 | /** Copy a gate condition from standard input to standard output | |
| 28 | * @return zero if everything is ok; nonzero on error | |
| 29 | */ | |
| 30 | static int | |
| 31 | parseGate (void) | |
| 32 | { | |
| 33 | int ch; | |
| 34 | loop: | |
| 35 | while (isspace (ch = fgetc (stdin))); | |
| 36 | fputc (ch, stdout); | |
| 37 | switch (ch) { | |
| 38 | case 't': | |
| 39 | case 'f': | |
| 40 | return 0; | |
| 41 | case '|': | |
| 42 | case '&': | |
| 43 | case 'i': | |
| 44 | case 'e': | |
| 45 | if (parseGate ()) | |
| 46 | return 1; | |
| 47 | case '!': | |
| 48 | goto loop; | |
| 49 | case 'p': | |
| 50 | if (1 != fscanf (stdin, "%d", &ch)) { | |
| 51 | fputs ("error in proposition number\n", stderr); | |
| 52 | return 1; | |
| 53 | } | |
| 54 | fprintf (stdout, "%d", ch); | |
| 55 | return 0; | |
| 56 | case EOF: | |
| 57 | fputs ("unexpected end of file while parsing formula\n", stderr); | |
| 58 | return 2; | |
| 59 | default: | |
| 60 | fprintf (stderr, "unknown character 0x%02x", ch); | |
| 61 | return 2; | |
| 62 | } | |
| 63 | } | |
| 64 | ||
| 65 | /** The main program | |
| 66 | * @param argc number of command-line arguments | |
| 67 | * @param argv the command-line arguments | |
| 68 | */ | |
| 69 | int | |
| 70 | main (int argc, char** argv) | |
| 71 | { | |
| 72 | /** State counter */ | |
| 73 | unsigned i; | |
| 74 | /** Generic number */ | |
| 75 | unsigned num; | |
| 76 | /** a character */ | |
| 77 | int ch; | |
| 78 | ||
| 79 | if (2 != fscanf (stdin, "%u%u", &i, &num)) { | |
| 80 | parseError: | |
| 81 | fputs ("error in automaton\n", stderr); | |
| 82 | semanticError: | |
| 83 | return 1; | |
| 84 | } | |
| 85 | ||
| 86 | fputs ("digraph g {\n", stdout); | |
| 87 | ||
| 88 | while (i--) { | |
| 89 | /** separator between acceptance set entries */ | |
| 90 | const char* separator = "\\n"; | |
| 91 | /** the state number */ | |
| 92 | unsigned state; | |
| 93 | /* read the state number and "initial state" flag */ | |
| 94 | if (2 != fscanf (stdin, "%u%u", &state, &num) || num > 1) | |
| 95 | goto parseError; | |
| 96 | fprintf (stdout, "%u", state); | |
| 97 | fputs ("[", stdout); | |
| 98 | if (num) /* initial state */ | |
| 99 | fputs ("style=filled,", stdout); | |
| 100 | fprintf (stdout, "label=\"%u", state); | |
| 101 | ||
| 102 | /* acceptance sets that the state belongs to */ | |
| 103 | for (;;) { | |
| 104 | while (isspace (ch = fgetc (stdin))); | |
| 105 | if (ch == '-') { | |
| 106 | if (1 != fscanf (stdin, "%u", &num) || 1 != num) { | |
| 107 | fputs ("unexpected data after '-'\n", stderr); | |
| 108 | goto semanticError; | |
| 109 | } | |
| 110 | break; | |
| 111 | } | |
| 112 | ungetc (ch, stdin); | |
| 113 | if (!isdigit (ch) || 1 != fscanf (stdin, "%u", &num)) | |
| 114 | goto parseError; | |
| 115 | fprintf (stdout, "%s%u", separator, num); | |
| 116 | separator = ","; | |
| 117 | } | |
| 118 | ||
| 119 | fputs ("\"];\n", stdout); | |
| 120 | ||
| 121 | /* transitions */ | |
| 122 | for (;;) { | |
| 123 | while (isspace (ch = fgetc (stdin))); | |
| 124 | if (ch == '-') { | |
| 125 | if (1 != fscanf (stdin, "%u", &num) || 1 != num) { | |
| 126 | fputs ("unexpected data after '-'\n", stderr); | |
| 127 | goto semanticError; | |
| 128 | } | |
| 129 | break; | |
| 130 | } | |
| 131 | ungetc (ch, stdin); | |
| 132 | if (!isdigit (ch) || 1 != fscanf (stdin, "%u", &num)) | |
| 133 | goto parseError; | |
| 134 | fprintf (stdout, "%u->%u[label=\"", state, num); | |
| 135 | if (parseGate ()) | |
| 136 | goto parseError; | |
| 137 | fputs ("\"];\n", stdout); | |
| 138 | } | |
| 139 | } | |
| 140 | ||
| 141 | fputs ("}\n", stdout); | |
| 142 | ||
| 143 | while (isspace (ch = fgetc (stdin))); | |
| 144 | ||
| 145 | if (ch != EOF) { | |
| 146 | fputs ("extraneous non-whitespace data at end of input\n", stderr); | |
| 147 | goto semanticError; | |
| 148 | } | |
| 149 | ||
| 150 | return 0; | |
| 151 | } |