From be18a22bce449bde5d5e6bb38418aca170e8fd3c Mon Sep 17 00:00:00 2001 From: Michael Weber Date: Wed, 3 Nov 2010 23:53:14 +0100 Subject: [PATCH] Import ltl2ba-1.1 http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ --- LICENSE | 222 +++++++++++++++++ Makefile | 42 ++++ README | 107 +++++++++ alternating.c | 443 ++++++++++++++++++++++++++++++++++ buchi.c | 653 ++++++++++++++++++++++++++++++++++++++++++++++++++ cache.c | 344 ++++++++++++++++++++++++++ generalized.c | 653 ++++++++++++++++++++++++++++++++++++++++++++++++++ lex.c | 184 ++++++++++++++ ltl2ba.h | 248 +++++++++++++++++++ main.c | 356 +++++++++++++++++++++++++++ mem.c | 245 +++++++++++++++++++ parse.c | 572 +++++++++++++++++++++++++++++++++++++++++++ rewrt.c | 326 +++++++++++++++++++++++++ set.c | 209 ++++++++++++++++ trans.c | 175 ++++++++++++++ 15 files changed, 4779 insertions(+) create mode 100644 LICENSE create mode 100644 Makefile create mode 100644 README create mode 100644 alternating.c create mode 100644 buchi.c create mode 100644 cache.c create mode 100644 generalized.c create mode 100644 lex.c create mode 100644 ltl2ba.h create mode 100644 main.c create mode 100644 mem.c create mode 100644 parse.c create mode 100644 rewrt.c create mode 100644 set.c create mode 100644 trans.c diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..3f06113 --- /dev/null +++ b/LICENSE @@ -0,0 +1,222 @@ + GNU GENERAL PUBLIC LICENSE + TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION + + 0. This License applies to any program or other work which contains +a notice placed by the copyright holder saying it may be distributed +under the terms of this General Public License. The "Program", below, +refers to any such program or work, and a "work based on the Program" +means either the Program or any derivative work under copyright law: +that is to say, a work containing the Program or a portion of it, +either verbatim or with modifications and/or translated into another +language. (Hereinafter, translation is included without limitation in +the term "modification".) Each licensee is addressed as "you". + +Activities other than copying, distribution and modification are not +covered by this License; they are outside its scope. The act of +running the Program is not restricted, and the output from the Program +is covered only if its contents constitute a work based on the +Program (independent of having been made by running the Program). +Whether that is true depends on what the Program does. + + 1. You may copy and distribute verbatim copies of the Program's +source code as you receive it, in any medium, provided that you +conspicuously and appropriately publish on each copy an appropriate +copyright notice and disclaimer of warranty; keep intact all the +notices that refer to this License and to the absence of any warranty; +and give any other recipients of the Program a copy of this License +along with the Program. + +You may charge a fee for the physical act of transferring a copy, and +you may at your option offer warranty protection in exchange for a fee. + + 2. You may modify your copy or copies of the Program or any portion +of it, thus forming a work based on the Program, and copy and +distribute such modifications or work under the terms of Section 1 +above, provided that you also meet all of these conditions: + + a) You must cause the modified files to carry prominent notices + stating that you changed the files and the date of any change. + + b) You must cause any work that you distribute or publish, that in + whole or in part contains or is derived from the Program or any + part thereof, to be licensed as a whole at no charge to all third + parties under the terms of this License. + + c) If the modified program normally reads commands interactively + when run, you must cause it, when started running for such + interactive use in the most ordinary way, to print or display an + announcement including an appropriate copyright notice and a + notice that there is no warranty (or else, saying that you provide + a warranty) and that users may redistribute the program under + these conditions, and telling the user how to view a copy of this + License. (Exception: if the Program itself is interactive but + does not normally print such an announcement, your work based on + the Program is not required to print an announcement.) + +These requirements apply to the modified work as a whole. If +identifiable sections of that work are not derived from the Program, +and can be reasonably considered independent and separate works in +themselves, then this License, and its terms, do not apply to those +sections when you distribute them as separate works. But when you +distribute the same sections as part of a whole which is a work based +on the Program, the distribution of the whole must be on the terms of +this License, whose permissions for other licensees extend to the +entire whole, and thus to each and every part regardless of who wrote it. + +Thus, it is not the intent of this section to claim rights or contest +your rights to work written entirely by you; rather, the intent is to +exercise the right to control the distribution of derivative or +collective works based on the Program. + +In addition, mere aggregation of another work not based on the Program +with the Program (or with a work based on the Program) on a volume of +a storage or distribution medium does not bring the other work under +the scope of this License. + + 3. You may copy and distribute the Program (or a work based on it, +under Section 2) in object code or executable form under the terms of +Sections 1 and 2 above provided that you also do one of the following: + + a) Accompany it with the complete corresponding machine-readable + source code, which must be distributed under the terms of Sections + 1 and 2 above on a medium customarily used for software interchange; or, + + b) Accompany it with a written offer, valid for at least three + years, to give any third party, for a charge no more than your + cost of physically performing source distribution, a complete + machine-readable copy of the corresponding source code, to be + distributed under the terms of Sections 1 and 2 above on a medium + customarily used for software interchange; or, + + c) Accompany it with the information you received as to the offer + to distribute corresponding source code. (This alternative is + allowed only for noncommercial distribution and only if you + received the program in object code or executable form with such + an offer, in accord with Subsection b above.) + +The source code for a work means the preferred form of the work for +making modifications to it. For an executable work, complete source +code means all the source code for all modules it contains, plus any +associated interface definition files, plus the scripts used to +control compilation and installation of the executable. However, as a +special exception, the source code distributed need not include +anything that is normally distributed (in either source or binary +form) with the major components (compiler, kernel, and so on) of the +operating system on which the executable runs, unless that component +itself accompanies the executable. + +If distribution of executable or object code is made by offering +access to copy from a designated place, then offering equivalent +access to copy the source code from the same place counts as +distribution of the source code, even though third parties are not +compelled to copy the source along with the object code. + + 4. You may not copy, modify, sublicense, or distribute the Program +except as expressly provided under this License. Any attempt +otherwise to copy, modify, sublicense or distribute the Program is +void, and will automatically terminate your rights under this License. +However, parties who have received copies, or rights, from you under +this License will not have their licenses terminated so long as such +parties remain in full compliance. + + 5. You are not required to accept this License, since you have not +signed it. However, nothing else grants you permission to modify or +distribute the Program or its derivative works. These actions are +prohibited by law if you do not accept this License. Therefore, by +modifying or distributing the Program (or any work based on the +Program), you indicate your acceptance of this License to do so, and +all its terms and conditions for copying, distributing or modifying +the Program or works based on it. + + 6. Each time you redistribute the Program (or any work based on the +Program), the recipient automatically receives a license from the +original licensor to copy, distribute or modify the Program subject to +these terms and conditions. You may not impose any further +restrictions on the recipients' exercise of the rights granted herein. +You are not responsible for enforcing compliance by third parties to +this License. + + 7. If, as a consequence of a court judgment or allegation of patent +infringement or for any other reason (not limited to patent issues), +conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot +distribute so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you +may not distribute the Program at all. For example, if a patent +license would not permit royalty-free redistribution of the Program by +all those who receive copies directly or indirectly through you, then +the only way you could satisfy both it and this License would be to +refrain entirely from distribution of the Program. + +If any portion of this section is held invalid or unenforceable under +any particular circumstance, the balance of the section is intended to +apply and the section as a whole is intended to apply in other +circumstances. + +It is not the purpose of this section to induce you to infringe any +patents or other property right claims or to contest validity of any +such claims; this section has the sole purpose of protecting the +integrity of the free software distribution system, which is +implemented by public license practices. Many people have made +generous contributions to the wide range of software distributed +through that system in reliance on consistent application of that +system; it is up to the author/donor to decide if he or she is willing +to distribute software through any other system and a licensee cannot +impose that choice. + +This section is intended to make thoroughly clear what is believed to +be a consequence of the rest of this License. + + 8. If the distribution and/or use of the Program is restricted in +certain countries either by patents or by copyrighted interfaces, the +original copyright holder who places the Program under this License +may add an explicit geographical distribution limitation excluding +those countries, so that distribution is permitted only in or among +countries not thus excluded. In such case, this License incorporates +the limitation as if written in the body of this License. + + 9. The Free Software Foundation may publish revised and/or new versions +of the General Public License from time to time. Such new versions will +be similar in spirit to the present version, but may differ in detail to +address new problems or concerns. + +Each version is given a distinguishing version number. If the Program +specifies a version number of this License which applies to it and "any +later version", you have the option of following the terms and conditions +either of that version or of any later version published by the Free +Software Foundation. If the Program does not specify a version number of +this License, you may choose any version ever published by the Free Software +Foundation. + + 10. If you wish to incorporate parts of the Program into other free +programs whose distribution conditions are different, write to the author +to ask for permission. For software which is copyrighted by the Free +Software Foundation, write to the Free Software Foundation; we sometimes +make exceptions for this. Our decision will be guided by the two goals +of preserving the free status of all derivatives of our free software and +of promoting the sharing and reuse of software generally. + + NO WARRANTY + + 11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY +FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN +OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES +PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED +OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF +MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS +TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE +PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, +REPAIR OR CORRECTION. + + 12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING +WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR +REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, +INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING +OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED +TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY +YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER +PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE +POSSIBILITY OF SUCH DAMAGES. + + END OF TERMS AND CONDITIONS diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..188b1c1 --- /dev/null +++ b/Makefile @@ -0,0 +1,42 @@ +# LTL2BA - Version 1.0 - October 2001 + +# Written by Denis Oddoux, LIAFA, France +# Copyright (c) 2001 Denis Oddoux +# +# 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., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA +# +# Based on the translation algorithm by Gastin and Oddoux, +# presented at the CAV Conference, held in 2001, Paris, France 2001. +# Send bug-reports and/or questions to: Denis.Oddoux@liafa.jussieu.fr +# or to Denis Oddoux +# LIAFA, UMR 7089, case 7014 +# Universite Paris 7 +# 2, place Jussieu +# F-75251 Paris Cedex 05 +# FRANCE + +CC=gcc +CFLAGS= -O3 -ansi -DNXT + +LTL2BA= parse.o lex.o main.o trans.o buchi.o set.o \ + mem.o rewrt.o cache.o alternating.o generalized.o + +ltl2ba: $(LTL2BA) + $(CC) $(CFLAGS) -o ltl2ba $(LTL2BA) + +$(LTL2BA): ltl2ba.h + +clean: + rm -f ltl2ba *.o core diff --git a/README b/README new file mode 100644 index 0000000..4f0c739 --- /dev/null +++ b/README @@ -0,0 +1,107 @@ +1. LICENSE + +LTL2BA - Version 1.0 - October 2001 +Written by Denis Oddoux, LIAFA, France +Copyright (c) 2001 Denis Oddoux + +LTL2BA - Version 1.1 - August 2007 +Modified by Paul Gastin, LSV, France +Copyright (c) 2007 Paul Gastin +Available at http://www.lsv.ens-cachan.fr/~gastin/ltl2ba + +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. GNU GPL is included in this +distribution, in a file called 'LICENSE' + +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., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA + +The LTL2BA software was written by Denis Oddoux and modified by Paul +Gastin. It is based on the translation algorithm presented at CAV '01: + P.Gastin and D.Oddoux + "Fast LTL to Büchi Automata Translation" + in 13th International Conference on Computer Aided Verification, CAV 2001, + G. Berry, H. Comon, A. Finkel (Eds.) + Paris, France, July 18-22, 2001, + Proceedings - LNCS 2102, pp. 53-65 + +Send bug-reports and/or questions to Paul Gastin +http://www.lsv.ens-cachan.fr/~gastin + +Part of the code included is issued from the SPIN software Version 3.4.1 +The SPIN software is written by Gerard J. Holzmann, originally as part +of ``Design and Validation of Protocols,'' ISBN 0-13-539925-4, +1991, Prentice Hall, Englewood Cliffs, NJ, 07632 +Here are the files that contain some code from Spin v3.4.1 : + + cache.c (originally tl_cache.c) + lex.c ( tl_lex.c ) + ltl2ba.h ( tl.h ) + main.c ( tl_main.c ) + mem.c ( tl_mem.c ) + parse.c ( tl_parse.c) + rewrt.c ( tl_rewrt.c) + trans.c ( tl_trans.c) + +2. COMPILING + +open the archive : +> gunzip ltl2ba-1.1.tar.gz +> tar xf ltl2ba-1.1.tar +> cd ltl2ba-1.1 + +compile the program +> make + +3. EXECUTING + +run the program +> ./ltl2ba -f "formula" + +The formula is an LTL formula, and may contain propositional symbols, +boolean operators, temporal operators, and parentheses. +The syntax used is the one used in the 'Spin' model-checker + +Propositonal Symbols: + true, false + any lowercase string + +Boolean operators: + ! (negation) + -> (implication) + <-> (equivalence) + && (and) + || (or) + +Temporal operators: + [] (always) + <> (eventually) + U (until) + V (release) + X (next) + +Use spaces between any symbols. + +The result is a never claim in Promela that can be given to the +Spin model checker to verify properties on a system. + +run the command +> ./ltl2ba +to see the possible options for executing the program + +4. CHANGES IN VERSION 1.1 + +- fixing a bug in the way sets were used for strongly connected components. Thanks to Joachim Klein (klein@tcs.inf.tu-dresden.de) who found the bug and proposed a patch to fix it. +- fixing a bug in the simplification with strongly connected components for the generalized Büchi automaton. +- improving the simplification with strongly connected components for the generalized Büchi automaton. +- using getrusage to compute running times for the statistics +- some other minor updates. + diff --git a/alternating.c b/alternating.c new file mode 100644 index 0000000..2dc947a --- /dev/null +++ b/alternating.c @@ -0,0 +1,443 @@ +/***** ltl2ba : alternating.c *****/ + +/* Written by Denis Oddoux, LIAFA, France */ +/* Copyright (c) 2001 Denis Oddoux */ +/* Modified by Paul Gastin, LSV, France */ +/* Copyright (c) 2007 Paul Gastin */ +/* */ +/* 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., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA*/ +/* */ +/* Based on the translation algorithm by Gastin and Oddoux, */ +/* presented at the 13th International Conference on Computer Aided */ +/* Verification, CAV 2001, Paris, France. */ +/* Proceedings - LNCS 2102, pp. 53-65 */ +/* */ +/* Send bug-reports and/or questions to Paul Gastin */ +/* http://www.lsv.ens-cachan.fr/~gastin */ + +#include "ltl2ba.h" + +/********************************************************************\ +|* Structures and shared variables *| +\********************************************************************/ + +extern FILE *tl_out; +extern int tl_verbose, tl_stats, tl_simp_diff; + +Node **label; +char **sym_table; +ATrans **transition; +struct rusage tr_debut, tr_fin; +struct timeval t_diff; +int *final_set, node_id = 1, sym_id = 0, node_size, sym_size; +int astate_count = 0, atrans_count = 0; + +ATrans *build_alternating(Node *p); + +/********************************************************************\ +|* Generation of the alternating automaton *| +\********************************************************************/ + +int calculate_node_size(Node *p) /* returns the number of temporal nodes */ +{ + switch(p->ntyp) { + case AND: + case OR: + case U_OPER: + case V_OPER: + return(calculate_node_size(p->lft) + calculate_node_size(p->rgt) + 1); +#ifdef NXT + case NEXT: + return(calculate_node_size(p->lft) + 1); +#endif + default: + return 1; + break; + } +} + +int calculate_sym_size(Node *p) /* returns the number of predicates */ +{ + switch(p->ntyp) { + case AND: + case OR: + case U_OPER: + case V_OPER: + return(calculate_sym_size(p->lft) + calculate_sym_size(p->rgt)); +#ifdef NXT + case NEXT: + return(calculate_sym_size(p->lft)); +#endif + case NOT: + case PREDICATE: + return 1; + default: + return 0; + } +} + +ATrans *dup_trans(ATrans *trans) /* returns the copy of a transition */ +{ + ATrans *result; + if(!trans) return trans; + result = emalloc_atrans(); + copy_set(trans->to, result->to, 0); + copy_set(trans->pos, result->pos, 1); + copy_set(trans->neg, result->neg, 1); + return result; +} + +void do_merge_trans(ATrans **result, ATrans *trans1, ATrans *trans2) +{ /* merges two transitions */ + if(!trans1 || !trans2) { + free_atrans(*result, 0); + *result = (ATrans *)0; + return; + } + if(!*result) + *result = emalloc_atrans(); + do_merge_sets((*result)->to, trans1->to, trans2->to, 0); + do_merge_sets((*result)->pos, trans1->pos, trans2->pos, 1); + do_merge_sets((*result)->neg, trans1->neg, trans2->neg, 1); + if(!empty_intersect_sets((*result)->pos, (*result)->neg, 1)) { + free_atrans(*result, 0); + *result = (ATrans *)0; + } +} + +ATrans *merge_trans(ATrans *trans1, ATrans *trans2) /* merges two transitions */ +{ + ATrans *result = emalloc_atrans(); + do_merge_trans(&result, trans1, trans2); + return result; +} + +int already_done(Node *p) /* finds the id of the node, if already explored */ +{ + int i; + for(i = 1; i next & init */ +{ + ATrans *t1, *t2, *lft, *rgt, *result = (ATrans *)0; + int id; + switch(p->ntyp) { + case TRUE: + result = emalloc_atrans(); + clear_set(result->to, 0); + clear_set(result->pos, 1); + clear_set(result->neg, 1); + case FALSE: + break; + case AND: + lft = boolean(p->lft); + rgt = boolean(p->rgt); + for(t1 = lft; t1; t1 = t1->nxt) { + for(t2 = rgt; t2; t2 = t2->nxt) { + ATrans *tmp = merge_trans(t1, t2); + if(tmp) { + tmp->nxt = result; + result = tmp; + } + } + } + free_atrans(lft, 1); + free_atrans(rgt, 1); + break; + case OR: + lft = boolean(p->lft); + for(t1 = lft; t1; t1 = t1->nxt) { + ATrans *tmp = dup_trans(t1); + tmp->nxt = result; + result = tmp; + } + free_atrans(lft, 1); + rgt = boolean(p->rgt); + for(t1 = rgt; t1; t1 = t1->nxt) { + ATrans *tmp = dup_trans(t1); + tmp->nxt = result; + result = tmp; + } + free_atrans(rgt, 1); + break; + default: + build_alternating(p); + result = emalloc_atrans(); + clear_set(result->to, 0); + clear_set(result->pos, 1); + clear_set(result->neg, 1); + add_set(result->to, already_done(p)); + } + return result; +} + +ATrans *build_alternating(Node *p) /* builds an alternating automaton for p */ +{ + ATrans *t1, *t2, *t = (ATrans *)0; + int node = already_done(p); + if(node >= 0) return transition[node]; + + switch (p->ntyp) { + + case TRUE: + t = emalloc_atrans(); + clear_set(t->to, 0); + clear_set(t->pos, 1); + clear_set(t->neg, 1); + case FALSE: + break; + + case PREDICATE: + t = emalloc_atrans(); + clear_set(t->to, 0); + clear_set(t->pos, 1); + clear_set(t->neg, 1); + add_set(t->pos, get_sym_id(p->sym->name)); + break; + + case NOT: + t = emalloc_atrans(); + clear_set(t->to, 0); + clear_set(t->pos, 1); + clear_set(t->neg, 1); + add_set(t->neg, get_sym_id(p->lft->sym->name)); + break; + +#ifdef NXT + case NEXT: + t = boolean(p->lft); + break; +#endif + + case U_OPER: /* p U q <-> q || (p && X (p U q)) */ + for(t2 = build_alternating(p->rgt); t2; t2 = t2->nxt) { + ATrans *tmp = dup_trans(t2); /* q */ + tmp->nxt = t; + t = tmp; + } + for(t1 = build_alternating(p->lft); t1; t1 = t1->nxt) { + ATrans *tmp = dup_trans(t1); /* p */ + add_set(tmp->to, node_id); /* X (p U q) */ + tmp->nxt = t; + t = tmp; + } + add_set(final_set, node_id); + break; + + case V_OPER: /* p V q <-> (p && q) || (p && X (p V q)) */ + for(t1 = build_alternating(p->rgt); t1; t1 = t1->nxt) { + ATrans *tmp; + + for(t2 = build_alternating(p->lft); t2; t2 = t2->nxt) { + tmp = merge_trans(t1, t2); /* p && q */ + if(tmp) { + tmp->nxt = t; + t = tmp; + } + } + + tmp = dup_trans(t1); /* p */ + add_set(tmp->to, node_id); /* X (p V q) */ + tmp->nxt = t; + t = tmp; + } + break; + + case AND: + t = (ATrans *)0; + for(t1 = build_alternating(p->lft); t1; t1 = t1->nxt) { + for(t2 = build_alternating(p->rgt); t2; t2 = t2->nxt) { + ATrans *tmp = merge_trans(t1, t2); + if(tmp) { + tmp->nxt = t; + t = tmp; + } + } + } + break; + + case OR: + t = (ATrans *)0; + for(t1 = build_alternating(p->lft); t1; t1 = t1->nxt) { + ATrans *tmp = dup_trans(t1); + tmp->nxt = t; + t = tmp; + } + for(t1 = build_alternating(p->rgt); t1; t1 = t1->nxt) { + ATrans *tmp = dup_trans(t1); + tmp->nxt = t; + t = tmp; + } + break; + + default: + break; + } + + transition[node_id] = t; + label[node_id++] = p; + return(t); +} + +/********************************************************************\ +|* Simplification of the alternating automaton *| +\********************************************************************/ + +void simplify_atrans(ATrans **trans) /* simplifies the transitions */ +{ + ATrans *t, *father = (ATrans *)0; + for(t = *trans; t;) { + ATrans *t1; + for(t1 = *trans; t1; t1 = t1->nxt) { + if((t1 != t) && + included_set(t1->to, t->to, 0) && + included_set(t1->pos, t->pos, 1) && + included_set(t1->neg, t->neg, 1)) + break; + } + if(t1) { + if (father) + father->nxt = t->nxt; + else + *trans = t->nxt; + free_atrans(t, 0); + if (father) + t = father->nxt; + else + t = *trans; + continue; + } + atrans_count++; + father = t; + t = t->nxt; + } +} + +void simplify_astates() /* simplifies the alternating automaton */ +{ + ATrans *t; + int i, *acc = make_set(-1, 0); /* no state is accessible initially */ + + for(t = transition[0]; t; t = t->nxt, i = 0) + merge_sets(acc, t->to, 0); /* all initial states are accessible */ + + for(i = node_id - 1; i > 0; i--) { + if (!in_set(acc, i)) { /* frees unaccessible states */ + label[i] = ZN; + free_atrans(transition[i], 1); + transition[i] = (ATrans *)0; + continue; + } + astate_count++; + simplify_atrans(&transition[i]); + for(t = transition[i]; t; t = t->nxt) + merge_sets(acc, t->to, 0); + } + + tfree(acc); +} + +/********************************************************************\ +|* Display of the alternating automaton *| +\********************************************************************/ + +void print_alternating() /* dumps the alternating automaton */ +{ + int i; + ATrans *t; + + fprintf(tl_out, "init :\n"); + for(t = transition[0]; t; t = t->nxt) { + print_set(t->to, 0); + fprintf(tl_out, "\n"); + } + + for(i = node_id - 1; i > 0; i--) { + if(!label[i]) + continue; + fprintf(tl_out, "state %i : ", i); + dump(label[i]); + fprintf(tl_out, "\n"); + for(t = transition[i]; t; t = t->nxt) { + if (empty_set(t->pos, 1) && empty_set(t->neg, 1)) + fprintf(tl_out, "1"); + print_set(t->pos, 1); + if (!empty_set(t->pos,1) && !empty_set(t->neg,1)) fprintf(tl_out, " & "); + print_set(t->neg, 2); + fprintf(tl_out, " -> "); + print_set(t->to, 0); + fprintf(tl_out, "\n"); + } + } +} + +/********************************************************************\ +|* Main method *| +\********************************************************************/ + +void mk_alternating(Node *p) /* generates an alternating automaton for p */ +{ + if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut); + + node_size = calculate_node_size(p) + 1; /* number of states in the automaton */ + label = (Node **) tl_emalloc(node_size * sizeof(Node *)); + transition = (ATrans **) tl_emalloc(node_size * sizeof(ATrans *)); + node_size = node_size / (8 * sizeof(int)) + 1; + + sym_size = calculate_sym_size(p); /* number of predicates */ + if(sym_size) sym_table = (char **) tl_emalloc(sym_size * sizeof(char *)); + sym_size = sym_size / (8 * sizeof(int)) + 1; + + final_set = make_set(-1, 0); + transition[0] = boolean(p); /* generates the alternating automaton */ + + if(tl_verbose) { + fprintf(tl_out, "\nAlternating automaton before simplification\n"); + print_alternating(); + } + + if(tl_simp_diff) { + simplify_astates(); /* keeps only accessible states */ + if(tl_verbose) { + fprintf(tl_out, "\nAlternating automaton after simplification\n"); + print_alternating(); + } + } + + if(tl_stats) { + getrusage(RUSAGE_SELF, &tr_fin); + timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime); + fprintf(tl_out, "\nBuilding and simplification of the alternating automaton: %i.%06is", + t_diff.tv_sec, t_diff.tv_usec); + fprintf(tl_out, "\n%i states, %i transitions\n", astate_count, atrans_count); + } + + releasenode(1, p); + tfree(label); +} diff --git a/buchi.c b/buchi.c new file mode 100644 index 0000000..fe1f80e --- /dev/null +++ b/buchi.c @@ -0,0 +1,653 @@ +/***** ltl2ba : buchi.c *****/ + +/* Written by Denis Oddoux, LIAFA, France */ +/* Copyright (c) 2001 Denis Oddoux */ +/* Modified by Paul Gastin, LSV, France */ +/* Copyright (c) 2007 Paul Gastin */ +/* */ +/* 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., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA*/ +/* */ +/* Based on the translation algorithm by Gastin and Oddoux, */ +/* presented at the 13th International Conference on Computer Aided */ +/* Verification, CAV 2001, Paris, France. */ +/* Proceedings - LNCS 2102, pp. 53-65 */ +/* */ +/* Send bug-reports and/or questions to Paul Gastin */ +/* http://www.lsv.ens-cachan.fr/~gastin */ + +#include "ltl2ba.h" + +/********************************************************************\ +|* Structures and shared variables *| +\********************************************************************/ + +extern GState **init, *gstates; +extern struct rusage tr_debut, tr_fin; +extern struct timeval t_diff; +extern int tl_verbose, tl_stats, tl_simp_diff, tl_simp_fly, tl_simp_scc, + init_size, *final; +extern void put_uform(void); + +extern FILE *tl_out; +BState *bstack, *bstates, *bremoved; +BScc *scc_stack; +int accept, bstate_count = 0, btrans_count = 0, rank; + +/********************************************************************\ +|* Simplification of the generalized Buchi automaton *| +\********************************************************************/ + +void free_bstate(BState *s) /* frees a state and its transitions */ +{ + free_btrans(s->trans->nxt, s->trans, 1); + tfree(s); +} + +BState *remove_bstate(BState *s, BState *s1) /* removes a state */ +{ + BState *prv = s->prv; + s->prv->nxt = s->nxt; + s->nxt->prv = s->prv; + free_btrans(s->trans->nxt, s->trans, 0); + s->trans = (BTrans *)0; + s->nxt = bremoved->nxt; + bremoved->nxt = s; + s->prv = s1; + for(s1 = bremoved->nxt; s1 != bremoved; s1 = s1->nxt) + if(s1->prv == s) + s1->prv = s->prv; + return prv; +} + +void copy_btrans(BTrans *from, BTrans *to) { + to->to = from->to; + copy_set(from->pos, to->pos, 1); + copy_set(from->neg, to->neg, 1); +} + +int simplify_btrans() /* simplifies the transitions */ +{ + BState *s; + BTrans *t, *t1; + int changed = 0; + + if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut); + + for (s = bstates->nxt; s != bstates; s = s->nxt) + for (t = s->trans->nxt; t != s->trans;) { + t1 = s->trans->nxt; + copy_btrans(t, s->trans); + while((t == t1) || (t->to != t1->to) || + !included_set(t1->pos, t->pos, 1) || + !included_set(t1->neg, t->neg, 1)) + t1 = t1->nxt; + if(t1 != s->trans) { + BTrans *free = t->nxt; + t->to = free->to; + copy_set(free->pos, t->pos, 1); + copy_set(free->neg, t->neg, 1); + t->nxt = free->nxt; + if(free == s->trans) s->trans = t; + free_btrans(free, 0, 0); + changed++; + } + else + t = t->nxt; + } + + if(tl_stats) { + getrusage(RUSAGE_SELF, &tr_fin); + timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime); + fprintf(tl_out, "\nSimplification of the Buchi automaton - transitions: %i.%06is", + t_diff.tv_sec, t_diff.tv_usec); + fprintf(tl_out, "\n%i transitions removed\n", changed); + + } + return changed; +} + +int same_btrans(BTrans *s, BTrans *t) /* returns 1 if the transitions are identical */ +{ + return((s->to == t->to) && + same_sets(s->pos, t->pos, 1) && + same_sets(s->neg, t->neg, 1)); +} + +void remove_btrans(BState *to) +{ /* redirects transitions before removing a state from the automaton */ + BState *s; + BTrans *t; + int i; + for (s = bstates->nxt; s != bstates; s = s->nxt) + for (t = s->trans->nxt; t != s->trans; t = t->nxt) + if (t->to == to) { /* transition to a state with no transitions */ + BTrans *free = t->nxt; + t->to = free->to; + copy_set(free->pos, t->pos, 1); + copy_set(free->neg, t->neg, 1); + t->nxt = free->nxt; + if(free == s->trans) s->trans = t; + free_btrans(free, 0, 0); + } +} + +void retarget_all_btrans() +{ /* redirects transitions before removing a state from the automaton */ + BState *s; + BTrans *t; + for (s = bstates->nxt; s != bstates; s = s->nxt) + for (t = s->trans->nxt; t != s->trans; t = t->nxt) + if (!t->to->trans) { /* t->to has been removed */ + t->to = t->to->prv; + if(!t->to) { /* t->to has no transitions */ + BTrans *free = t->nxt; + t->to = free->to; + copy_set(free->pos, t->pos, 1); + copy_set(free->neg, t->neg, 1); + t->nxt = free->nxt; + if(free == s->trans) s->trans = t; + free_btrans(free, 0, 0); + } + } + while(bremoved->nxt != bremoved) { /* clean the 'removed' list */ + s = bremoved->nxt; + bremoved->nxt = bremoved->nxt->nxt; + tfree(s); + } +} + +int all_btrans_match(BState *a, BState *b) /* decides if the states are equivalent */ +{ + BTrans *s, *t; + if (((a->final == accept) || (b->final == accept)) && + (a->final + b->final != 2 * accept) && + a->incoming >=0 && b->incoming >=0) + return 0; /* the states have to be both final or both non final */ + + for (s = a->trans->nxt; s != a->trans; s = s->nxt) { + /* all transitions from a appear in b */ + copy_btrans(s, b->trans); + t = b->trans->nxt; + while(!same_btrans(s, t)) + t = t->nxt; + if(t == b->trans) return 0; + } + for (s = b->trans->nxt; s != b->trans; s = s->nxt) { + /* all transitions from b appear in a */ + copy_btrans(s, a->trans); + t = a->trans->nxt; + while(!same_btrans(s, t)) + t = t->nxt; + if(t == a->trans) return 0; + } + return 1; +} + +int simplify_bstates() /* eliminates redundant states */ +{ + BState *s, *s1; + int changed = 0; + + if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut); + + for (s = bstates->nxt; s != bstates; s = s->nxt) { + if(s->trans == s->trans->nxt) { /* s has no transitions */ + s = remove_bstate(s, (BState *)0); + changed++; + continue; + } + bstates->trans = s->trans; + bstates->final = s->final; + s1 = s->nxt; + while(!all_btrans_match(s, s1)) + s1 = s1->nxt; + if(s1 != bstates) { /* s and s1 are equivalent */ + if(s1->incoming == -1) + s1->final = s->final; /* get the good final condition */ + s = remove_bstate(s, s1); + changed++; + } + } + retarget_all_btrans(); + + if(tl_stats) { + getrusage(RUSAGE_SELF, &tr_fin); + timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime); + fprintf(tl_out, "\nSimplification of the Buchi automaton - states: %i.%06is", + t_diff.tv_sec, t_diff.tv_usec); + fprintf(tl_out, "\n%i states removed\n", changed); + } + + return changed; +} + +int bdfs(BState *s) { + BTrans *t; + BScc *c; + BScc *scc = (BScc *)tl_emalloc(sizeof(BScc)); + scc->bstate = s; + scc->rank = rank; + scc->theta = rank++; + scc->nxt = scc_stack; + scc_stack = scc; + + s->incoming = 1; + + for (t = s->trans->nxt; t != s->trans; t = t->nxt) { + if (t->to->incoming == 0) { + int result = bdfs(t->to); + scc->theta = min(scc->theta, result); + } + else { + for(c = scc_stack->nxt; c != 0; c = c->nxt) + if(c->bstate == t->to) { + scc->theta = min(scc->theta, c->rank); + break; + } + } + } + if(scc->rank == scc->theta) { + if(scc_stack == scc) { /* s is alone in a scc */ + s->incoming = -1; + for (t = s->trans->nxt; t != s->trans; t = t->nxt) + if (t->to == s) + s->incoming = 1; + } + scc_stack = scc->nxt; + } + return scc->theta; +} + +void simplify_bscc() { + BState *s; + rank = 1; + scc_stack = 0; + + if(bstates == bstates->nxt) return; + + for(s = bstates->nxt; s != bstates; s = s->nxt) + s->incoming = 0; /* state color = white */ + + bdfs(bstates->prv); + + for(s = bstates->nxt; s != bstates; s = s->nxt) + if(s->incoming == 0) + remove_bstate(s, 0); +} + + + + +/********************************************************************\ +|* Generation of the Buchi automaton *| +\********************************************************************/ + +BState *find_bstate(GState **state, int final, BState *s) +{ /* finds the corresponding state, or creates it */ + if((s->gstate == *state) && (s->final == final)) return s; /* same state */ + + s = bstack->nxt; /* in the stack */ + bstack->gstate = *state; + bstack->final = final; + while(!(s->gstate == *state) || !(s->final == final)) + s = s->nxt; + if(s != bstack) return s; + + s = bstates->nxt; /* in the solved states */ + bstates->gstate = *state; + bstates->final = final; + while(!(s->gstate == *state) || !(s->final == final)) + s = s->nxt; + if(s != bstates) return s; + + s = bremoved->nxt; /* in the removed states */ + bremoved->gstate = *state; + bremoved->final = final; + while(!(s->gstate == *state) || !(s->final == final)) + s = s->nxt; + if(s != bremoved) return s; + + s = (BState *)tl_emalloc(sizeof(BState)); /* creates a new state */ + s->gstate = *state; + s->id = (*state)->id; + s->incoming = 0; + s->final = final; + s->trans = emalloc_btrans(); /* sentinel */ + s->trans->nxt = s->trans; + s->nxt = bstack->nxt; + bstack->nxt = s; + return s; +} + +int next_final(int *set, int fin) /* computes the 'final' value */ +{ + if((fin != accept) && in_set(set, final[fin + 1])) + return next_final(set, fin + 1); + return fin; +} + +void make_btrans(BState *s) /* creates all the transitions from a state */ +{ + int state_trans = 0; + GTrans *t; + BTrans *t1; + BState *s1; + if(s->gstate->trans) + for(t = s->gstate->trans->nxt; t != s->gstate->trans; t = t->nxt) { + int fin = next_final(t->final, (s->final == accept) ? 0 : s->final); + BState *to = find_bstate(&t->to, fin, s); + + for(t1 = s->trans->nxt; t1 != s->trans;) { + if(tl_simp_fly && + (to == t1->to) && + included_set(t->pos, t1->pos, 1) && + included_set(t->neg, t1->neg, 1)) { /* t1 is redondant */ + BTrans *free = t1->nxt; + t1->to->incoming--; + t1->to = free->to; + copy_set(free->pos, t1->pos, 1); + copy_set(free->neg, t1->neg, 1); + t1->nxt = free->nxt; + if(free == s->trans) s->trans = t1; + free_btrans(free, 0, 0); + state_trans--; + } + else if(tl_simp_fly && + (t1->to == to ) && + included_set(t1->pos, t->pos, 1) && + included_set(t1->neg, t->neg, 1)) /* t is redondant */ + break; + else + t1 = t1->nxt; + } + if(t1 == s->trans) { + BTrans *trans = emalloc_btrans(); + trans->to = to; + trans->to->incoming++; + copy_set(t->pos, trans->pos, 1); + copy_set(t->neg, trans->neg, 1); + trans->nxt = s->trans->nxt; + s->trans->nxt = trans; + state_trans++; + } + } + + if(tl_simp_fly) { + if(s->trans == s->trans->nxt) { /* s has no transitions */ + free_btrans(s->trans->nxt, s->trans, 1); + s->trans = (BTrans *)0; + s->prv = (BState *)0; + s->nxt = bremoved->nxt; + bremoved->nxt = s; + for(s1 = bremoved->nxt; s1 != bremoved; s1 = s1->nxt) + if(s1->prv == s) + s1->prv = (BState *)0; + return; + } + bstates->trans = s->trans; + bstates->final = s->final; + s1 = bstates->nxt; + while(!all_btrans_match(s, s1)) + s1 = s1->nxt; + if(s1 != bstates) { /* s and s1 are equivalent */ + free_btrans(s->trans->nxt, s->trans, 1); + s->trans = (BTrans *)0; + s->prv = s1; + s->nxt = bremoved->nxt; + bremoved->nxt = s; + for(s1 = bremoved->nxt; s1 != bremoved; s1 = s1->nxt) + if(s1->prv == s) + s1->prv = s->prv; + return; + } + } + s->nxt = bstates->nxt; /* adds the current state to 'bstates' */ + s->prv = bstates; + s->nxt->prv = s; + bstates->nxt = s; + btrans_count += state_trans; + bstate_count++; +} + +/********************************************************************\ +|* Display of the Buchi automaton *| +\********************************************************************/ + +void print_buchi(BState *s) /* dumps the Buchi automaton */ +{ + BTrans *t; + if(s == bstates) return; + + print_buchi(s->nxt); /* begins with the last state */ + + fprintf(tl_out, "state "); + if(s->id == -1) + fprintf(tl_out, "init"); + else { + if(s->final == accept) + fprintf(tl_out, "accept"); + else + fprintf(tl_out, "T%i", s->final); + fprintf(tl_out, "_%i", s->id); + } + fprintf(tl_out, "\n"); + for(t = s->trans->nxt; t != s->trans; t = t->nxt) { + if (empty_set(t->pos, 1) && empty_set(t->neg, 1)) + fprintf(tl_out, "1"); + print_set(t->pos, 1); + if (!empty_set(t->pos, 1) && !empty_set(t->neg, 1)) fprintf(tl_out, " & "); + print_set(t->neg, 2); + fprintf(tl_out, " -> "); + if(t->to->id == -1) + fprintf(tl_out, "init\n"); + else { + if(t->to->final == accept) + fprintf(tl_out, "accept"); + else + fprintf(tl_out, "T%i", t->to->final); + fprintf(tl_out, "_%i\n", t->to->id); + } + } +} + +void print_spin_buchi() { + BTrans *t; + BState *s; + int accept_all = 0, init_count = 0; + if(bstates->nxt == bstates) { /* empty automaton */ + fprintf(tl_out, "never { /* "); + put_uform(); + fprintf(tl_out, " */\n"); + fprintf(tl_out, "T0_init:\n"); + fprintf(tl_out, "\tfalse;\n"); + fprintf(tl_out, "}\n"); + return; + } + if(bstates->nxt->nxt == bstates && bstates->nxt->id == 0) { /* true */ + fprintf(tl_out, "never { /* "); + put_uform(); + fprintf(tl_out, " */\n"); + fprintf(tl_out, "accept_init:\n"); + fprintf(tl_out, "\tif\n"); + fprintf(tl_out, "\t:: (1) -> goto accept_init\n"); + fprintf(tl_out, "\tfi;\n"); + fprintf(tl_out, "}\n"); + return; + } + + fprintf(tl_out, "never { /* "); + put_uform(); + fprintf(tl_out, " */\n"); + for(s = bstates->prv; s != bstates; s = s->prv) { + if(s->id == 0) { /* accept_all at the end */ + accept_all = 1; + continue; + } + if(s->final == accept) + fprintf(tl_out, "accept_"); + else fprintf(tl_out, "T%i_", s->final); + if(s->id == -1) + fprintf(tl_out, "init:\n"); + else fprintf(tl_out, "S%i:\n", s->id); + if(s->trans->nxt == s->trans) { + fprintf(tl_out, "\tfalse;\n"); + continue; + } + fprintf(tl_out, "\tif\n"); + for(t = s->trans->nxt; t != s->trans; t = t->nxt) { + BTrans *t1; + fprintf(tl_out, "\t:: ("); + spin_print_set(t->pos, t->neg); + for(t1 = t; t1->nxt != s->trans; ) + if (t1->nxt->to->id == t->to->id && + t1->nxt->to->final == t->to->final) { + fprintf(tl_out, ") || ("); + spin_print_set(t1->nxt->pos, t1->nxt->neg); + t1->nxt = t1->nxt->nxt; + } + else t1 = t1->nxt; + fprintf(tl_out, ") -> goto "); + if(t->to->final == accept) + fprintf(tl_out, "accept_"); + else fprintf(tl_out, "T%i_", t->to->final); + if(t->to->id == 0) + fprintf(tl_out, "all\n"); + else if(t->to->id == -1) + fprintf(tl_out, "init\n"); + else fprintf(tl_out, "S%i\n", t->to->id); + } + fprintf(tl_out, "\tfi;\n"); + } + if(accept_all) { + fprintf(tl_out, "accept_all:\n"); + fprintf(tl_out, "\tskip\n"); + } + fprintf(tl_out, "}\n"); +} + +/********************************************************************\ +|* Main method *| +\********************************************************************/ + +void mk_buchi() +{/* generates a Buchi automaton from the generalized Buchi automaton */ + int i; + BState *s = (BState *)tl_emalloc(sizeof(BState)); + GTrans *t; + BTrans *t1; + accept = final[0] - 1; + + if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut); + + bstack = (BState *)tl_emalloc(sizeof(BState)); /* sentinel */ + bstack->nxt = bstack; + bremoved = (BState *)tl_emalloc(sizeof(BState)); /* sentinel */ + bremoved->nxt = bremoved; + bstates = (BState *)tl_emalloc(sizeof(BState)); /* sentinel */ + bstates->nxt = s; + bstates->prv = s; + + s->nxt = bstates; /* creates (unique) inital state */ + s->prv = bstates; + s->id = -1; + s->incoming = 1; + s->final = 0; + s->gstate = 0; + s->trans = emalloc_btrans(); /* sentinel */ + s->trans->nxt = s->trans; + for(i = 0; i < init_size; i++) + if(init[i]) + for(t = init[i]->trans->nxt; t != init[i]->trans; t = t->nxt) { + int fin = next_final(t->final, 0); + BState *to = find_bstate(&t->to, fin, s); + for(t1 = s->trans->nxt; t1 != s->trans;) { + if(tl_simp_fly && + (to == t1->to) && + included_set(t->pos, t1->pos, 1) && + included_set(t->neg, t1->neg, 1)) { /* t1 is redondant */ + BTrans *free = t1->nxt; + t1->to->incoming--; + t1->to = free->to; + copy_set(free->pos, t1->pos, 1); + copy_set(free->neg, t1->neg, 1); + t1->nxt = free->nxt; + if(free == s->trans) s->trans = t1; + free_btrans(free, 0, 0); + } + else if(tl_simp_fly && + (t1->to == to ) && + included_set(t1->pos, t->pos, 1) && + included_set(t1->neg, t->neg, 1)) /* t is redondant */ + break; + else + t1 = t1->nxt; + } + if(t1 == s->trans) { + BTrans *trans = emalloc_btrans(); + trans->to = to; + trans->to->incoming++; + copy_set(t->pos, trans->pos, 1); + copy_set(t->neg, trans->neg, 1); + trans->nxt = s->trans->nxt; + s->trans->nxt = trans; + } + } + + while(bstack->nxt != bstack) { /* solves all states in the stack until it is empty */ + s = bstack->nxt; + bstack->nxt = bstack->nxt->nxt; + if(!s->incoming) { + free_bstate(s); + continue; + } + make_btrans(s); + } + + retarget_all_btrans(); + + if(tl_stats) { + getrusage(RUSAGE_SELF, &tr_fin); + timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime); + fprintf(tl_out, "\nBuilding the Buchi automaton : %i.%06is", + t_diff.tv_sec, t_diff.tv_usec); + fprintf(tl_out, "\n%i states, %i transitions\n", bstate_count, btrans_count); + } + + if(tl_verbose) { + fprintf(tl_out, "\nBuchi automaton before simplification\n"); + print_buchi(bstates->nxt); + if(bstates == bstates->nxt) + fprintf(tl_out, "empty automaton, refuses all words\n"); + } + + if(tl_simp_diff) { + simplify_btrans(); + if(tl_simp_scc) simplify_bscc(); + while(simplify_bstates()) { /* simplifies as much as possible */ + simplify_btrans(); + if(tl_simp_scc) simplify_bscc(); + } + + if(tl_verbose) { + fprintf(tl_out, "\nBuchi automaton after simplification\n"); + print_buchi(bstates->nxt); + if(bstates == bstates->nxt) + fprintf(tl_out, "empty automaton, refuses all words\n"); + fprintf(tl_out, "\n"); + } + } + + print_spin_buchi(); +} diff --git a/cache.c b/cache.c new file mode 100644 index 0000000..a71f518 --- /dev/null +++ b/cache.c @@ -0,0 +1,344 @@ +/***** ltl2ba : cache.c *****/ + +/* Written by Denis Oddoux, LIAFA, France */ +/* Copyright (c) 2001 Denis Oddoux */ +/* Modified by Paul Gastin, LSV, France */ +/* Copyright (c) 2007 Paul Gastin */ +/* */ +/* 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., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA*/ +/* */ +/* Based on the translation algorithm by Gastin and Oddoux, */ +/* presented at the 13th International Conference on Computer Aided */ +/* Verification, CAV 2001, Paris, France. */ +/* Proceedings - LNCS 2102, pp. 53-65 */ +/* */ +/* Send bug-reports and/or questions to Paul Gastin */ +/* http://www.lsv.ens-cachan.fr/~gastin */ +/* */ +/* Some of the code in this file was taken from the Spin software */ +/* Written by Gerard J. Holzmann, Bell Laboratories, U.S.A. */ + +#include "ltl2ba.h" + +typedef struct Cache { + Node *before; + Node *after; + int same; + struct Cache *nxt; +} Cache; + +static Cache *stored = (Cache *) 0; +static unsigned long Caches, CacheHits; + +static int ismatch(Node *, Node *); +extern void fatal(char *, char *); +int sameform(Node *, Node *); + +void +cache_dump(void) +{ Cache *d; int nr=0; + + printf("\nCACHE DUMP:\n"); + for (d = stored; d; d = d->nxt, nr++) + { if (d->same) continue; + printf("B%3d: ", nr); dump(d->before); printf("\n"); + printf("A%3d: ", nr); dump(d->after); printf("\n"); + } + printf("============\n"); +} + +Node * +in_cache(Node *n) +{ Cache *d; int nr=0; + + for (d = stored; d; d = d->nxt, nr++) + if (isequal(d->before, n)) + { CacheHits++; + if (d->same && ismatch(n, d->before)) return n; + return dupnode(d->after); + } + return ZN; +} + +Node * +cached(Node *n) +{ Cache *d; + Node *m; + + if (!n) return n; + if (m = in_cache(n)) + return m; + + Caches++; + d = (Cache *) tl_emalloc(sizeof(Cache)); + d->before = dupnode(n); + d->after = Canonical(n); /* n is released */ + + if (ismatch(d->before, d->after)) + { d->same = 1; + releasenode(1, d->after); + d->after = d->before; + } + d->nxt = stored; + stored = d; + return dupnode(d->after); +} + +void +cache_stats(void) +{ + printf("cache stores : %9ld\n", Caches); + printf("cache hits : %9ld\n", CacheHits); +} + +void +releasenode(int all_levels, Node *n) +{ + if (!n) return; + + if (all_levels) + { releasenode(1, n->lft); + n->lft = ZN; + releasenode(1, n->rgt); + n->rgt = ZN; + } + tfree((void *) n); +} + +Node * +tl_nn(int t, Node *ll, Node *rl) +{ Node *n = (Node *) tl_emalloc(sizeof(Node)); + + n->ntyp = (short) t; + n->lft = ll; + n->rgt = rl; + + return n; +} + +Node * +getnode(Node *p) +{ Node *n; + + if (!p) return p; + + n = (Node *) tl_emalloc(sizeof(Node)); + n->ntyp = p->ntyp; + n->sym = p->sym; /* same name */ + n->lft = p->lft; + n->rgt = p->rgt; + + return n; +} + +Node * +dupnode(Node *n) +{ Node *d; + + if (!n) return n; + d = getnode(n); + d->lft = dupnode(n->lft); + d->rgt = dupnode(n->rgt); + return d; +} + +int +one_lft(int ntyp, Node *x, Node *in) +{ + if (!x) return 1; + if (!in) return 0; + + if (sameform(x, in)) + return 1; + + if (in->ntyp != ntyp) + return 0; + + if (one_lft(ntyp, x, in->lft)) + return 1; + + return one_lft(ntyp, x, in->rgt); +} + +int +all_lfts(int ntyp, Node *from, Node *in) +{ + if (!from) return 1; + + if (from->ntyp != ntyp) + return one_lft(ntyp, from, in); + + if (!one_lft(ntyp, from->lft, in)) + return 0; + + return all_lfts(ntyp, from->rgt, in); +} + +int +sametrees(int ntyp, Node *a, Node *b) +{ /* toplevel is an AND or OR */ + /* both trees are right-linked, but the leafs */ + /* can be in different places in the two trees */ + + if (!all_lfts(ntyp, a, b)) + return 0; + + return all_lfts(ntyp, b, a); +} + +int /* a better isequal() */ +sameform(Node *a, Node *b) +{ + if (!a && !b) return 1; + if (!a || !b) return 0; + if (a->ntyp != b->ntyp) return 0; + + if (a->sym + && b->sym + && strcmp(a->sym->name, b->sym->name) != 0) + return 0; + + switch (a->ntyp) { + case TRUE: + case FALSE: + return 1; + case PREDICATE: + if (!a->sym || !b->sym) fatal("sameform...", (char *) 0); + return !strcmp(a->sym->name, b->sym->name); + + case NOT: +#ifdef NXT + case NEXT: +#endif + return sameform(a->lft, b->lft); + case U_OPER: + case V_OPER: + if (!sameform(a->lft, b->lft)) + return 0; + if (!sameform(a->rgt, b->rgt)) + return 0; + return 1; + + case AND: + case OR: /* the hard case */ + return sametrees(a->ntyp, a, b); + + default: + printf("type: %d\n", a->ntyp); + fatal("cannot happen, sameform", (char *) 0); + } + + return 0; +} + +int +isequal(Node *a, Node *b) +{ + if (!a && !b) + return 1; + + if (!a || !b) + { if (!a) + { if (b->ntyp == TRUE) + return 1; + } else + { if (a->ntyp == TRUE) + return 1; + } + return 0; + } + if (a->ntyp != b->ntyp) + return 0; + + if (a->sym + && b->sym + && strcmp(a->sym->name, b->sym->name) != 0) + return 0; + + if (isequal(a->lft, b->lft) + && isequal(a->rgt, b->rgt)) + return 1; + + return sameform(a, b); +} + +static int +ismatch(Node *a, Node *b) +{ + if (!a && !b) return 1; + if (!a || !b) return 0; + if (a->ntyp != b->ntyp) return 0; + + if (a->sym + && b->sym + && strcmp(a->sym->name, b->sym->name) != 0) + return 0; + + if (ismatch(a->lft, b->lft) + && ismatch(a->rgt, b->rgt)) + return 1; + + return 0; +} + +int +any_term(Node *srch, Node *in) +{ + if (!in) return 0; + + if (in->ntyp == AND) + return any_term(srch, in->lft) || + any_term(srch, in->rgt); + + return isequal(in, srch); +} + +int +any_and(Node *srch, Node *in) +{ + if (!in) return 0; + + if (srch->ntyp == AND) + return any_and(srch->lft, in) && + any_and(srch->rgt, in); + + return any_term(srch, in); +} + +int +any_lor(Node *srch, Node *in) +{ + if (!in) return 0; + + if (in->ntyp == OR) + return any_lor(srch, in->lft) || + any_lor(srch, in->rgt); + + return isequal(in, srch); +} + +int +anywhere(int tok, Node *srch, Node *in) +{ + if (!in) return 0; + + switch (tok) { + case AND: return any_and(srch, in); + case OR: return any_lor(srch, in); + case 0: return any_term(srch, in); + } + fatal("cannot happen, anywhere", (char *) 0); + return 0; +} diff --git a/generalized.c b/generalized.c new file mode 100644 index 0000000..6a37fe2 --- /dev/null +++ b/generalized.c @@ -0,0 +1,653 @@ +/***** ltl2ba : generalized.c *****/ + +/* Written by Denis Oddoux, LIAFA, France */ +/* Copyright (c) 2001 Denis Oddoux */ +/* Modified by Paul Gastin, LSV, France */ +/* Copyright (c) 2007 Paul Gastin */ +/* */ +/* 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., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA*/ +/* */ +/* Based on the translation algorithm by Gastin and Oddoux, */ +/* presented at the 13th International Conference on Computer Aided */ +/* Verification, CAV 2001, Paris, France. */ +/* Proceedings - LNCS 2102, pp. 53-65 */ +/* */ +/* Send bug-reports and/or questions to Paul Gastin */ +/* http://www.lsv.ens-cachan.fr/~gastin */ + +#include "ltl2ba.h" + +/********************************************************************\ +|* Structures and shared variables *| +\********************************************************************/ + +extern FILE *tl_out; +extern ATrans **transition; +extern struct rusage tr_debut, tr_fin; +extern struct timeval t_diff; +extern int tl_verbose, tl_stats, tl_simp_diff, tl_simp_fly, tl_fjtofj, + tl_simp_scc, *final_set, node_id; +extern char **sym_table; + +GState *gstack, *gremoved, *gstates, **init; +GScc *scc_stack; +int init_size = 0, gstate_id = 1, gstate_count = 0, gtrans_count = 0; +int *fin, *final, rank, scc_id, scc_size, *bad_scc; + +void print_generalized(); + +/********************************************************************\ +|* Simplification of the generalized Buchi automaton *| +\********************************************************************/ + +void free_gstate(GState *s) /* frees a state and its transitions */ +{ + free_gtrans(s->trans->nxt, s->trans, 1); + tfree(s->nodes_set); + tfree(s); +} + +GState *remove_gstate(GState *s, GState *s1) /* removes a state */ +{ + GState *prv = s->prv; + s->prv->nxt = s->nxt; + s->nxt->prv = s->prv; + free_gtrans(s->trans->nxt, s->trans, 0); + s->trans = (GTrans *)0; + tfree(s->nodes_set); + s->nodes_set = 0; + s->nxt = gremoved->nxt; + gremoved->nxt = s; + s->prv = s1; + for(s1 = gremoved->nxt; s1 != gremoved; s1 = s1->nxt) + if(s1->prv == s) + s1->prv = s->prv; + return prv; +} + +void copy_gtrans(GTrans *from, GTrans *to) /* copies a transition */ +{ + to->to = from->to; + copy_set(from->pos, to->pos, 1); + copy_set(from->neg, to->neg, 1); + copy_set(from->final, to->final, 0); +} + +int same_gtrans(GState *a, GTrans *s, GState *b, GTrans *t, int use_scc) +{ /* returns 1 if the transitions are identical */ + if((s->to != t->to) || + ! same_sets(s->pos, t->pos, 1) || + ! same_sets(s->neg, t->neg, 1)) + return 0; /* transitions differ */ + if(same_sets(s->final, t->final, 0)) + return 1; /* same transitions exactly */ + /* next we check whether acceptance conditions may be ignored */ + if( use_scc && + ( in_set(bad_scc, a->incoming) || + in_set(bad_scc, b->incoming) || + (a->incoming != s->to->incoming) || + (b->incoming != t->to->incoming) ) ) + return 1; + return 0; + /* below is the old test to check whether acceptance conditions may be ignored */ + if(!use_scc) + return 0; /* transitions differ */ + if( (a->incoming == b->incoming) && (a->incoming == s->to->incoming) ) + return 0; /* same scc: acceptance conditions must be taken into account */ + /* if scc(a)=scc(b)>scc(s->to) then acceptance conditions need not be taken into account */ + /* if scc(a)>scc(b) and scc(a) is non-trivial then all_gtrans_match(a,b,use_scc) will fail */ + /* if scc(a) is trivial then acceptance conditions of transitions from a need not be taken into account */ + return 1; /* same transitions up to acceptance conditions */ +} + +int simplify_gtrans() /* simplifies the transitions */ +{ + int changed = 0; + GState *s; + GTrans *t, *t1; + + if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut); + + for(s = gstates->nxt; s != gstates; s = s->nxt) { + t = s->trans->nxt; + while(t != s->trans) { /* tries to remove t */ + copy_gtrans(t, s->trans); + t1 = s->trans->nxt; + while ( !((t != t1) + && (t1->to == t->to) + && included_set(t1->pos, t->pos, 1) + && included_set(t1->neg, t->neg, 1) + && (included_set(t->final, t1->final, 0) /* acceptance conditions of t are also in t1 or may be ignored */ + || (tl_simp_scc && ((s->incoming != t->to->incoming) || in_set(bad_scc, s->incoming))))) ) + t1 = t1->nxt; + if(t1 != s->trans) { /* remove transition t */ + GTrans *free = t->nxt; + t->to = free->to; + copy_set(free->pos, t->pos, 1); + copy_set(free->neg, t->neg, 1); + copy_set(free->final, t->final, 0); + t->nxt = free->nxt; + if(free == s->trans) s->trans = t; + free_gtrans(free, 0, 0); + changed++; + } + else + t = t->nxt; + } + } + + if(tl_stats) { + getrusage(RUSAGE_SELF, &tr_fin); + timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime); + fprintf(tl_out, "\nSimplification of the generalized Buchi automaton - transitions: %i.%06is", + t_diff.tv_sec, t_diff.tv_usec); + fprintf(tl_out, "\n%i transitions removed\n", changed); + } + + return changed; +} + +void retarget_all_gtrans() +{ /* redirects transitions before removing a state from the automaton */ + GState *s; + GTrans *t; + int i; + for (i = 0; i < init_size; i++) + if (init[i] && !init[i]->trans) /* init[i] has been removed */ + init[i] = init[i]->prv; + for (s = gstates->nxt; s != gstates; s = s->nxt) + for (t = s->trans->nxt; t != s->trans; ) + if (!t->to->trans) { /* t->to has been removed */ + t->to = t->to->prv; + if(!t->to) { /* t->to has no transitions */ + GTrans *free = t->nxt; + t->to = free->to; + copy_set(free->pos, t->pos, 1); + copy_set(free->neg, t->neg, 1); + copy_set(free->final, t->final, 0); + t->nxt = free->nxt; + if(free == s->trans) s->trans = t; + free_gtrans(free, 0, 0); + } + else + t = t->nxt; + } + else + t = t->nxt; + while(gremoved->nxt != gremoved) { /* clean the 'removed' list */ + s = gremoved->nxt; + gremoved->nxt = gremoved->nxt->nxt; + if(s->nodes_set) tfree(s->nodes_set); + tfree(s); + } +} + +int all_gtrans_match(GState *a, GState *b, int use_scc) +{ /* decides if the states are equivalent */ + GTrans *s, *t; + for (s = a->trans->nxt; s != a->trans; s = s->nxt) { + /* all transitions from a appear in b */ + copy_gtrans(s, b->trans); + t = b->trans->nxt; + while(!same_gtrans(a, s, b, t, use_scc)) t = t->nxt; + if(t == b->trans) return 0; + } + for (t = b->trans->nxt; t != b->trans; t = t->nxt) { + /* all transitions from b appear in a */ + copy_gtrans(t, a->trans); + s = a->trans->nxt; + while(!same_gtrans(a, s, b, t, use_scc)) s = s->nxt; + if(s == a->trans) return 0; + } + return 1; +} + +int simplify_gstates() /* eliminates redundant states */ +{ + int changed = 0; + GState *a, *b; + + if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut); + + for(a = gstates->nxt; a != gstates; a = a->nxt) { + if(a->trans == a->trans->nxt) { /* a has no transitions */ + a = remove_gstate(a, (GState *)0); + changed++; + continue; + } + gstates->trans = a->trans; + b = a->nxt; + while(!all_gtrans_match(a, b, tl_simp_scc)) b = b->nxt; + if(b != gstates) { /* a and b are equivalent */ + /* if scc(a)>scc(b) and scc(a) is non-trivial then all_gtrans_match(a,b,use_scc) must fail */ + if(a->incoming > b->incoming) /* scc(a) is trivial */ + a = remove_gstate(a, b); + else /* either scc(a)=scc(b) or scc(b) is trivial */ + remove_gstate(b, a); + changed++; + } + } + retarget_all_gtrans(); + + if(tl_stats) { + getrusage(RUSAGE_SELF, &tr_fin); + timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime); + fprintf(tl_out, "\nSimplification of the generalized Buchi automaton - states: %i.%06is", + t_diff.tv_sec, t_diff.tv_usec); + fprintf(tl_out, "\n%i states removed\n", changed); + } + + return changed; +} + +int gdfs(GState *s) { + GTrans *t; + GScc *c; + GScc *scc = (GScc *)tl_emalloc(sizeof(GScc)); + scc->gstate = s; + scc->rank = rank; + scc->theta = rank++; + scc->nxt = scc_stack; + scc_stack = scc; + + s->incoming = 1; + + for (t = s->trans->nxt; t != s->trans; t = t->nxt) { + if (t->to->incoming == 0) { + int result = gdfs(t->to); + scc->theta = min(scc->theta, result); + } + else { + for(c = scc_stack->nxt; c != 0; c = c->nxt) + if(c->gstate == t->to) { + scc->theta = min(scc->theta, c->rank); + break; + } + } + } + if(scc->rank == scc->theta) { + while(scc_stack != scc) { + scc_stack->gstate->incoming = scc_id; + scc_stack = scc_stack->nxt; + } + scc->gstate->incoming = scc_id++; + scc_stack = scc->nxt; + } + return scc->theta; +} + +void simplify_gscc() { + GState *s; + GTrans *t; + int i, **scc_final; + rank = 1; + scc_stack = 0; + scc_id = 1; + + if(gstates == gstates->nxt) return; + + for(s = gstates->nxt; s != gstates; s = s->nxt) + s->incoming = 0; /* state color = white */ + + for(i = 0; i < init_size; i++) + if(init[i] && init[i]->incoming == 0) + gdfs(init[i]); + + scc_final = (int **)tl_emalloc(scc_id * sizeof(int *)); + for(i = 0; i < scc_id; i++) + scc_final[i] = make_set(-1,0); + + for(s = gstates->nxt; s != gstates; s = s->nxt) + if(s->incoming == 0) + s = remove_gstate(s, 0); + else + for (t = s->trans->nxt; t != s->trans; t = t->nxt) + if(t->to->incoming == s->incoming) + merge_sets(scc_final[s->incoming], t->final, 0); + + scc_size = (scc_id + 1) / (8 * sizeof(int)) + 1; + bad_scc=make_set(-1,2); + + for(i = 0; i < scc_id; i++) + if(!included_set(final_set, scc_final[i], 0)) + add_set(bad_scc, i); + + for(i = 0; i < scc_id; i++) + tfree(scc_final[i]); + tfree(scc_final); +} + +/********************************************************************\ +|* Generation of the generalized Buchi automaton *| +\********************************************************************/ + +int is_final(int *from, ATrans *at, int i) /*is the transition final for i ?*/ +{ + ATrans *t; + int in_to; + if((tl_fjtofj && !in_set(at->to, i)) || + (!tl_fjtofj && !in_set(from, i))) return 1; + in_to = in_set(at->to, i); + rem_set(at->to, i); + for(t = transition[i]; t; t = t->nxt) + if(included_set(t->to, at->to, 0) && + included_set(t->pos, at->pos, 1) && + included_set(t->neg, at->neg, 1)) { + if(in_to) add_set(at->to, i); + return 1; + } + if(in_to) add_set(at->to, i); + return 0; +} + +GState *find_gstate(int *set, GState *s) +{ /* finds the corresponding state, or creates it */ + + if(same_sets(set, s->nodes_set, 0)) return s; /* same state */ + + s = gstack->nxt; /* in the stack */ + gstack->nodes_set = set; + while(!same_sets(set, s->nodes_set, 0)) + s = s->nxt; + if(s != gstack) return s; + + s = gstates->nxt; /* in the solved states */ + gstates->nodes_set = set; + while(!same_sets(set, s->nodes_set, 0)) + s = s->nxt; + if(s != gstates) return s; + + s = gremoved->nxt; /* in the removed states */ + gremoved->nodes_set = set; + while(!same_sets(set, s->nodes_set, 0)) + s = s->nxt; + if(s != gremoved) return s; + + s = (GState *)tl_emalloc(sizeof(GState)); /* creates a new state */ + s->id = (empty_set(set, 0)) ? 0 : gstate_id++; + s->incoming = 0; + s->nodes_set = dup_set(set, 0); + s->trans = emalloc_gtrans(); /* sentinel */ + s->trans->nxt = s->trans; + s->nxt = gstack->nxt; + gstack->nxt = s; + return s; +} + +void make_gtrans(GState *s) { /* creates all the transitions from a state */ + int i, *list, state_trans = 0, trans_exist = 1; + GState *s1; + GTrans *t; + ATrans *t1, *free; + AProd *prod = (AProd *)tl_emalloc(sizeof(AProd)); /* initialization */ + prod->nxt = prod; + prod->prv = prod; + prod->prod = emalloc_atrans(); + clear_set(prod->prod->to, 0); + clear_set(prod->prod->pos, 1); + clear_set(prod->prod->neg, 1); + prod->trans = prod->prod; + prod->trans->nxt = prod->prod; + list = list_set(s->nodes_set, 0); + + for(i = 1; i < list[0]; i++) { + AProd *p = (AProd *)tl_emalloc(sizeof(AProd)); + p->astate = list[i]; + p->trans = transition[list[i]]; + if(!p->trans) trans_exist = 0; + p->prod = merge_trans(prod->nxt->prod, p->trans); + p->nxt = prod->nxt; + p->prv = prod; + p->nxt->prv = p; + p->prv->nxt = p; + } + + while(trans_exist) { /* calculates all the transitions */ + AProd *p = prod->nxt; + t1 = p->prod; + if(t1) { /* solves the current transition */ + GTrans *trans, *t2; + clear_set(fin, 0); + for(i = 1; i < final[0]; i++) + if(is_final(s->nodes_set, t1, final[i])) + add_set(fin, final[i]); + for(t2 = s->trans->nxt; t2 != s->trans;) { + if(tl_simp_fly && + included_set(t1->to, t2->to->nodes_set, 0) && + included_set(t1->pos, t2->pos, 1) && + included_set(t1->neg, t2->neg, 1) && + same_sets(fin, t2->final, 0)) { /* t2 is redondant */ + GTrans *free = t2->nxt; + t2->to->incoming--; + t2->to = free->to; + copy_set(free->pos, t2->pos, 1); + copy_set(free->neg, t2->neg, 1); + copy_set(free->final, t2->final, 0); + t2->nxt = free->nxt; + if(free == s->trans) s->trans = t2; + free_gtrans(free, 0, 0); + state_trans--; + } + else if(tl_simp_fly && + included_set(t2->to->nodes_set, t1->to, 0) && + included_set(t2->pos, t1->pos, 1) && + included_set(t2->neg, t1->neg, 1) && + same_sets(t2->final, fin, 0)) {/* t1 is redondant */ + break; + } + else { + t2 = t2->nxt; + } + } + if(t2 == s->trans) { /* adds the transition */ + trans = emalloc_gtrans(); + trans->to = find_gstate(t1->to, s); + trans->to->incoming++; + copy_set(t1->pos, trans->pos, 1); + copy_set(t1->neg, trans->neg, 1); + copy_set(fin, trans->final, 0); + trans->nxt = s->trans->nxt; + s->trans->nxt = trans; + state_trans++; + } + } + if(!p->trans) + break; + while(!p->trans->nxt) /* calculates the next transition */ + p = p->nxt; + if(p == prod) + break; + p->trans = p->trans->nxt; + do_merge_trans(&(p->prod), p->nxt->prod, p->trans); + p = p->prv; + while(p != prod) { + p->trans = transition[p->astate]; + do_merge_trans(&(p->prod), p->nxt->prod, p->trans); + p = p->prv; + } + } + + tfree(list); /* free memory */ + while(prod->nxt != prod) { + AProd *p = prod->nxt; + prod->nxt = p->nxt; + free_atrans(p->prod, 0); + tfree(p); + } + free_atrans(prod->prod, 0); + tfree(prod); + + if(tl_simp_fly) { + if(s->trans == s->trans->nxt) { /* s has no transitions */ + free_gtrans(s->trans->nxt, s->trans, 1); + s->trans = (GTrans *)0; + s->prv = (GState *)0; + s->nxt = gremoved->nxt; + gremoved->nxt = s; + for(s1 = gremoved->nxt; s1 != gremoved; s1 = s1->nxt) + if(s1->prv == s) + s1->prv = (GState *)0; + return; + } + + gstates->trans = s->trans; + s1 = gstates->nxt; + while(!all_gtrans_match(s, s1, 0)) + s1 = s1->nxt; + if(s1 != gstates) { /* s and s1 are equivalent */ + free_gtrans(s->trans->nxt, s->trans, 1); + s->trans = (GTrans *)0; + s->prv = s1; + s->nxt = gremoved->nxt; + gremoved->nxt = s; + for(s1 = gremoved->nxt; s1 != gremoved; s1 = s1->nxt) + if(s1->prv == s) + s1->prv = s->prv; + return; + } + } + + s->nxt = gstates->nxt; /* adds the current state to 'gstates' */ + s->prv = gstates; + s->nxt->prv = s; + gstates->nxt = s; + gtrans_count += state_trans; + gstate_count++; +} + +/********************************************************************\ +|* Display of the generalized Buchi automaton *| +\********************************************************************/ + +void reverse_print_generalized(GState *s) /* dumps the generalized Buchi automaton */ +{ + GTrans *t; + if(s == gstates) return; + + reverse_print_generalized(s->nxt); /* begins with the last state */ + + fprintf(tl_out, "state %i (", s->id); + print_set(s->nodes_set, 0); + fprintf(tl_out, ") : %i\n", s->incoming); + for(t = s->trans->nxt; t != s->trans; t = t->nxt) { + if (empty_set(t->pos, 1) && empty_set(t->neg, 1)) + fprintf(tl_out, "1"); + print_set(t->pos, 1); + if (!empty_set(t->pos, 1) && !empty_set(t->neg, 1)) fprintf(tl_out, " & "); + print_set(t->neg, 1); + fprintf(tl_out, " -> %i : ", t->to->id); + print_set(t->final, 0); + fprintf(tl_out, "\n"); + } +} + +void print_generalized() { /* prints intial states and calls 'reverse_print' */ + int i; + fprintf(tl_out, "init :\n"); + for(i = 0; i < init_size; i++) + if(init[i]) + fprintf(tl_out, "%i\n", init[i]->id); + reverse_print_generalized(gstates->nxt); +} + +/********************************************************************\ +|* Main method *| +\********************************************************************/ + +void mk_generalized() +{ /* generates a generalized Buchi automaton from the alternating automaton */ + ATrans *t; + GState *s; + int i; + + if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut); + + fin = new_set(0); + bad_scc = 0; /* will be initialized in simplify_gscc */ + final = list_set(final_set, 0); + + gstack = (GState *)tl_emalloc(sizeof(GState)); /* sentinel */ + gstack->nxt = gstack; + gremoved = (GState *)tl_emalloc(sizeof(GState)); /* sentinel */ + gremoved->nxt = gremoved; + gstates = (GState *)tl_emalloc(sizeof(GState)); /* sentinel */ + gstates->nxt = gstates; + gstates->prv = gstates; + + for(t = transition[0]; t; t = t->nxt) { /* puts initial states in the stack */ + s = (GState *)tl_emalloc(sizeof(GState)); + s->id = (empty_set(t->to, 0)) ? 0 : gstate_id++; + s->incoming = 1; + s->nodes_set = dup_set(t->to, 0); + s->trans = emalloc_gtrans(); /* sentinel */ + s->trans->nxt = s->trans; + s->nxt = gstack->nxt; + gstack->nxt = s; + init_size++; + } + + if(init_size) init = (GState **)tl_emalloc(init_size * sizeof(GState *)); + init_size = 0; + for(s = gstack->nxt; s != gstack; s = s->nxt) + init[init_size++] = s; + + while(gstack->nxt != gstack) { /* solves all states in the stack until it is empty */ + s = gstack->nxt; + gstack->nxt = gstack->nxt->nxt; + if(!s->incoming) { + free_gstate(s); + continue; + } + make_gtrans(s); + } + + retarget_all_gtrans(); + + if(tl_stats) { + getrusage(RUSAGE_SELF, &tr_fin); + timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime); + fprintf(tl_out, "\nBuilding the generalized Buchi automaton : %i.%06is", + t_diff.tv_sec, t_diff.tv_usec); + fprintf(tl_out, "\n%i states, %i transitions\n", gstate_count, gtrans_count); + } + + tfree(gstack); + /*for(i = 0; i < node_id; i++) /* frees the data from the alternating automaton */ + /*free_atrans(transition[i], 1);*/ + free_all_atrans(); + tfree(transition); + + if(tl_verbose) { + fprintf(tl_out, "\nGeneralized Buchi automaton before simplification\n"); + print_generalized(); + } + + if(tl_simp_diff) { + if (tl_simp_scc) simplify_gscc(); + simplify_gtrans(); + if (tl_simp_scc) simplify_gscc(); + while(simplify_gstates()) { /* simplifies as much as possible */ + if (tl_simp_scc) simplify_gscc(); + simplify_gtrans(); + if (tl_simp_scc) simplify_gscc(); + } + + if(tl_verbose) { + fprintf(tl_out, "\nGeneralized Buchi automaton after simplification\n"); + print_generalized(); + } + } +} + diff --git a/lex.c b/lex.c new file mode 100644 index 0000000..06ee423 --- /dev/null +++ b/lex.c @@ -0,0 +1,184 @@ +/***** ltl2ba : lex.c *****/ + +/* Written by Denis Oddoux, LIAFA, France */ +/* Copyright (c) 2001 Denis Oddoux */ +/* Modified by Paul Gastin, LSV, France */ +/* Copyright (c) 2007 Paul Gastin */ +/* */ +/* 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., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA*/ +/* */ +/* Based on the translation algorithm by Gastin and Oddoux, */ +/* presented at the 13th International Conference on Computer Aided */ +/* Verification, CAV 2001, Paris, France. */ +/* Proceedings - LNCS 2102, pp. 53-65 */ +/* */ +/* Send bug-reports and/or questions to Paul Gastin */ +/* http://www.lsv.ens-cachan.fr/~gastin */ +/* */ +/* Some of the code in this file was taken from the Spin software */ +/* Written by Gerard J. Holzmann, Bell Laboratories, U.S.A. */ + +#include +#include +#include "ltl2ba.h" + +static Symbol *symtab[Nhash+1]; +static int tl_lex(void); + +extern YYSTYPE tl_yylval; +char yytext[2048]; + +#define Token(y) tl_yylval = tl_nn(y,ZN,ZN); return y + +int +isalnum_(int c) +{ return (isalnum(c) || c == '_'); +} + +int +hash(char *s) +{ int h=0; + + while (*s) + { h += *s++; + h <<= 1; + if (h&(Nhash+1)) + h |= 1; + } + return h&Nhash; +} + +static void +getword(int first, int (*tst)(int)) +{ int i=0; char c; + + yytext[i++]= (char ) first; + while (tst(c = tl_Getchar())) + yytext[i++] = c; + yytext[i] = '\0'; + tl_UnGetchar(); +} + +static int +follow(int tok, int ifyes, int ifno) +{ int c; + char buf[32]; + extern int tl_yychar; + + if ((c = tl_Getchar()) == tok) + return ifyes; + tl_UnGetchar(); + tl_yychar = c; + sprintf(buf, "expected '%c'", tok); + tl_yyerror(buf); /* no return from here */ + return ifno; +} + +int +tl_yylex(void) +{ int c = tl_lex(); +#if 0 + printf("c = %d\n", c); +#endif + return c; +} + +static int +tl_lex(void) +{ int c; + + do { + c = tl_Getchar(); + yytext[0] = (char ) c; + yytext[1] = '\0'; + + if (c <= 0) + { Token(';'); + } + + } while (c == ' '); /* '\t' is removed in tl_main.c */ + + if (islower(c)) + { getword(c, isalnum_); + if (strcmp("true", yytext) == 0) + { Token(TRUE); + } + if (strcmp("false", yytext) == 0) + { Token(FALSE); + } + tl_yylval = tl_nn(PREDICATE,ZN,ZN); + tl_yylval->sym = tl_lookup(yytext); + return PREDICATE; + } + if (c == '<') + { c = tl_Getchar(); + if (c == '>') + { Token(EVENTUALLY); + } + if (c != '-') + { tl_UnGetchar(); + tl_yyerror("expected '<>' or '<->'"); + } + c = tl_Getchar(); + if (c == '>') + { Token(EQUIV); + } + tl_UnGetchar(); + tl_yyerror("expected '<->'"); + } + + switch (c) { + case '/' : c = follow('\\', AND, '/'); break; + case '\\': c = follow('/', OR, '\\'); break; + case '&' : c = follow('&', AND, '&'); break; + case '|' : c = follow('|', OR, '|'); break; + case '[' : c = follow(']', ALWAYS, '['); break; + case '-' : c = follow('>', IMPLIES, '-'); break; + case '!' : c = NOT; break; + case 'U' : c = U_OPER; break; + case 'V' : c = V_OPER; break; +#ifdef NXT + case 'X' : c = NEXT; break; +#endif + default : break; + } + Token(c); +} + +Symbol * +tl_lookup(char *s) +{ Symbol *sp; + int h = hash(s); + + for (sp = symtab[h]; sp; sp = sp->next) + if (strcmp(sp->name, s) == 0) + return sp; + + sp = (Symbol *) tl_emalloc(sizeof(Symbol)); + sp->name = (char *) tl_emalloc(strlen(s) + 1); + strcpy(sp->name, s); + sp->next = symtab[h]; + symtab[h] = sp; + + return sp; +} + +Symbol * +getsym(Symbol *s) +{ Symbol *n = (Symbol *) tl_emalloc(sizeof(Symbol)); + + n->name = s->name; + return n; +} diff --git a/ltl2ba.h b/ltl2ba.h new file mode 100644 index 0000000..0987643 --- /dev/null +++ b/ltl2ba.h @@ -0,0 +1,248 @@ +/***** ltl2ba : ltl2ba.h *****/ + +/* Written by Denis Oddoux, LIAFA, France */ +/* Copyright (c) 2001 Denis Oddoux */ +/* Modified by Paul Gastin, LSV, France */ +/* Copyright (c) 2007 Paul Gastin */ +/* */ +/* 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., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA*/ +/* */ +/* Based on the translation algorithm by Gastin and Oddoux, */ +/* presented at the 13th International Conference on Computer Aided */ +/* Verification, CAV 2001, Paris, France. */ +/* Proceedings - LNCS 2102, pp. 53-65 */ +/* */ +/* Send bug-reports and/or questions to Paul Gastin */ +/* http://www.lsv.ens-cachan.fr/~gastin */ +/* */ +/* Some of the code in this file was taken from the Spin software */ +/* Written by Gerard J. Holzmann, Bell Laboratories, U.S.A. */ + +#include +#include +#include +#include +#include + +typedef struct Symbol { +char *name; + struct Symbol *next; /* linked list, symbol table */ +} Symbol; + +typedef struct Node { + short ntyp; /* node type */ + struct Symbol *sym; + struct Node *lft; /* tree */ + struct Node *rgt; /* tree */ + struct Node *nxt; /* if linked list */ +} Node; + +typedef struct Graph { + Symbol *name; + Symbol *incoming; + Symbol *outgoing; + Symbol *oldstring; + Symbol *nxtstring; + Node *New; + Node *Old; + Node *Other; + Node *Next; + unsigned char isred[64], isgrn[64]; + unsigned char redcnt, grncnt; + unsigned char reachable; + struct Graph *nxt; +} Graph; + +typedef struct Mapping { + char *from; + Graph *to; + struct Mapping *nxt; +} Mapping; + +typedef struct ATrans { + int *to; + int *pos; + int *neg; + struct ATrans *nxt; +} ATrans; + +typedef struct AProd { + int astate; + struct ATrans *prod; + struct ATrans *trans; + struct AProd *nxt; + struct AProd *prv; +} AProd; + + +typedef struct GTrans { + int *pos; + int *neg; + struct GState *to; + int *final; + struct GTrans *nxt; +} GTrans; + +typedef struct GState { + int id; + int incoming; + int *nodes_set; + struct GTrans *trans; + struct GState *nxt; + struct GState *prv; +} GState; + +typedef struct BTrans { + struct BState *to; + int *pos; + int *neg; + struct BTrans *nxt; +} BTrans; + +typedef struct BState { + struct GState *gstate; + int id; + int incoming; + int final; + struct BTrans *trans; + struct BState *nxt; + struct BState *prv; +} BState; + +typedef struct GScc { + struct GState *gstate; + int rank; + int theta; + struct GScc *nxt; +} GScc; + +typedef struct BScc { + struct BState *bstate; + int rank; + int theta; + struct BScc *nxt; +} BScc; + +enum { + ALWAYS=257, + AND, /* 258 */ + EQUIV, /* 259 */ + EVENTUALLY, /* 260 */ + FALSE, /* 261 */ + IMPLIES, /* 262 */ + NOT, /* 263 */ + OR, /* 264 */ + PREDICATE, /* 265 */ + TRUE, /* 266 */ + U_OPER, /* 267 */ + V_OPER /* 268 */ +#ifdef NXT + , NEXT /* 269 */ +#endif +}; + +Node *Canonical(Node *); +Node *canonical(Node *); +Node *cached(Node *); +Node *dupnode(Node *); +Node *getnode(Node *); +Node *in_cache(Node *); +Node *push_negation(Node *); +Node *right_linked(Node *); +Node *tl_nn(int, Node *, Node *); + +Symbol *tl_lookup(char *); +Symbol *getsym(Symbol *); +Symbol *DoDump(Node *); + +char *emalloc(int); + +int anywhere(int, Node *, Node *); +int dump_cond(Node *, Node *, int); +int isequal(Node *, Node *); +int tl_Getchar(void); + +void *tl_emalloc(int); +ATrans *emalloc_atrans(); +void free_atrans(ATrans *, int); +void free_all_atrans(); +GTrans *emalloc_gtrans(); +void free_gtrans(GTrans *, GTrans *, int); +BTrans *emalloc_btrans(); +void free_btrans(BTrans *, BTrans *, int); +void a_stats(void); +void addtrans(Graph *, char *, Node *, char *); +void cache_stats(void); +void dump(Node *); +void exit(int); +void Fatal(char *, char *); +void fatal(char *, char *); +void fsm_print(void); +void releasenode(int, Node *); +void tfree(void *); +void tl_explain(int); +void tl_UnGetchar(void); +void tl_parse(void); +void tl_yyerror(char *); +void trans(Node *); + +void mk_alternating(Node *); +void mk_generalized(); +void mk_buchi(); + +ATrans *dup_trans(ATrans *); +ATrans *merge_trans(ATrans *, ATrans *); +void do_merge_trans(ATrans **, ATrans *, ATrans *); + +int *new_set(int); +int *clear_set(int *, int); +int *make_set(int , int); +void copy_set(int *, int *, int); +int *dup_set(int *, int); +void merge_sets(int *, int *, int); +void do_merge_sets(int *, int *, int *, int); +int *intersect_sets(int *, int *, int); +void add_set(int *, int); +void rem_set(int *, int); +void spin_print_set(int *, int*); +void print_set(int *, int); +int empty_set(int *, int); +int empty_intersect_sets(int *, int *, int); +int same_sets(int *, int *, int); +int included_set(int *, int *, int); +int in_set(int *, int); +int *list_set(int *, int); + +int timeval_subtract (struct timeval *, struct timeval *, struct timeval *); + +#define ZN (Node *)0 +#define ZS (Symbol *)0 +#define Nhash 255 +#define True tl_nn(TRUE, ZN, ZN) +#define False tl_nn(FALSE, ZN, ZN) +#define Not(a) push_negation(tl_nn(NOT, a, ZN)) +#define rewrite(n) canonical(right_linked(n)) + +typedef Node *Nodeptr; +#define YYSTYPE Nodeptr + +#define Debug(x) { if (0) printf(x); } +#define Debug2(x,y) { if (tl_verbose) printf(x,y); } +#define Dump(x) { if (0) dump(x); } +#define Explain(x) { if (tl_verbose) tl_explain(x); } + +#define Assert(x, y) { if (!(x)) { tl_explain(y); \ + Fatal(": assertion failed\n",(char *)0); } } +#define min(x,y) ((x 0) + (void) unlink((const char *)out1); + exit(estatus); +} + +FILE * +cpyfile(char *src, char *tgt) +{ FILE *inp, *out; + char buf[1024]; + + inp = fopen(src, "r"); + out = fopen(tgt, "w"); + if (!inp || !out) + { printf("ltl2ba: cannot cp %s to %s\n", src, tgt); + alldone(1); + } + while (fgets(buf, 1024, inp)) + fprintf(out, "%s", buf); + fclose(inp); + return out; +} + +char * +emalloc(int n) +{ char *tmp; + + if (!(tmp = (char *) malloc(n))) + fatal("not enough memory", (char *)0); + memset(tmp, 0, n); + return tmp; +} + +int +tl_Getchar(void) +{ + if (cnt < hasuform) + return uform[cnt++]; + cnt++; + return -1; +} + +void +put_uform(void) +{ + fprintf(tl_out, "%s", uform); +} + +void +tl_UnGetchar(void) +{ + if (cnt > 0) cnt--; +} + +void +usage(void) +{ + printf("usage: ltl2ba [-flag] -f formula\n"); + printf(" or -F file\n"); + printf(" -f \"formula\"\ttranslate LTL "); + printf("into never claim\n"); + printf(" -F file\tlike -f, but with the LTL "); + printf("formula stored in a 1-line file\n"); + printf(" -d\t\tdisplay automata (D)escription at each step\n"); + printf(" -s\t\tcomputing time and automata sizes (S)tatistics\n"); + printf(" -l\t\tdisable (L)ogic formula simplification\n"); + printf(" -p\t\tdisable a-(P)osteriori simplification\n"); + printf(" -o\t\tdisable (O)n-the-fly simplification\n"); + printf(" -c\t\tdisable strongly (C)onnected components simplification\n"); + printf(" -a\t\tdisable trick in (A)ccepting conditions\n"); + + alldone(1); +} + +int +tl_main(int argc, char *argv[]) +{ int i; + while (argc > 1 && argv[1][0] == '-') + { switch (argv[1][1]) { + case 'f': argc--; argv++; + for (i = 0; i < argv[1][i]; i++) + { if (argv[1][i] == '\t' + || argv[1][i] == '\"' + || argv[1][i] == '\n') + argv[1][i] = ' '; + } + strcpy(uform, argv[1]); + hasuform = strlen(uform); + break; + default : usage(); + } + argc--; argv++; + } + if (hasuform == 0) usage(); + tl_parse(); + if (tl_stats) tl_endstats(); + return tl_errs; +} + +int +main(int argc, char *argv[]) +{ int i; + tl_out = stdout; + + while (argc > 1 && argv[1][0] == '-') + { switch (argv[1][1]) { + case 'F': ltl_file = (char **) (argv+2); + argc--; argv++; break; + case 'f': add_ltl = (char **) argv; + argc--; argv++; break; + case 'a': tl_fjtofj = 0; break; + case 'c': tl_simp_scc = 0; break; + case 'o': tl_simp_fly = 0; break; + case 'p': tl_simp_diff = 0; break; + case 'l': tl_simp_log = 0; break; + case 'd': tl_verbose = 1; break; + case 's': tl_stats = 1; break; + default : usage(); break; + } + argc--, argv++; + } + + if(!ltl_file && !add_ltl) usage(); + + if (ltl_file) + { char formula[4096]; + add_ltl = ltl_file-2; add_ltl[1][1] = 'f'; + if (!(tl_out = fopen(*ltl_file, "r"))) + { printf("ltl2ba: cannot open %s\n", *ltl_file); + alldone(1); + } + fgets(formula, 4096, tl_out); + fclose(tl_out); + tl_out = stdout; + *ltl_file = (char *) formula; + } + if (argc > 1) + { char cmd[128], out2[64]; + strcpy(out1, "_tmp1_"); + strcpy(out2, "_tmp2_"); + tl_out = cpyfile(argv[1], out2); + tl_main(2, add_ltl); + fclose(tl_out); + } else + { + if (argc > 0) + exit(tl_main(2, add_ltl)); + usage(); + } +} + +/* Subtract the `struct timeval' values X and Y, storing the result X-Y in RESULT. + Return 1 if the difference is negative, otherwise 0. */ + +int +timeval_subtract (result, x, y) +struct timeval *result, *x, *y; +{ + if (x->tv_usec < y->tv_usec) { + x->tv_usec += 1000000; + x->tv_sec--; + } + + /* Compute the time remaining to wait. tv_usec is certainly positive. */ + result->tv_sec = x->tv_sec - y->tv_sec; + result->tv_usec = x->tv_usec - y->tv_usec; + + /* Return 1 if result is negative. */ + return x->tv_sec < y->tv_sec; +} + +static void +tl_endstats(void) +{ extern int Stack_mx; + printf("\ntotal memory used: %9ld\n", All_Mem); + /*printf("largest stack sze: %9d\n", Stack_mx);*/ + /*cache_stats();*/ + a_stats(); +} + +#define Binop(a) \ + fprintf(tl_out, "("); \ + dump(n->lft); \ + fprintf(tl_out, a); \ + dump(n->rgt); \ + fprintf(tl_out, ")") + +void +dump(Node *n) +{ + if (!n) return; + + switch(n->ntyp) { + case OR: Binop(" || "); break; + case AND: Binop(" && "); break; + case U_OPER: Binop(" U "); break; + case V_OPER: Binop(" V "); break; +#ifdef NXT + case NEXT: + fprintf(tl_out, "X"); + fprintf(tl_out, " ("); + dump(n->lft); + fprintf(tl_out, ")"); + break; +#endif + case NOT: + fprintf(tl_out, "!"); + fprintf(tl_out, " ("); + dump(n->lft); + fprintf(tl_out, ")"); + break; + case FALSE: + fprintf(tl_out, "false"); + break; + case TRUE: + fprintf(tl_out, "true"); + break; + case PREDICATE: + fprintf(tl_out, "(%s)", n->sym->name); + break; + case -1: + fprintf(tl_out, " D "); + break; + default: + printf("Unknown token: "); + tl_explain(n->ntyp); + break; + } +} + +void +tl_explain(int n) +{ + switch (n) { + case ALWAYS: printf("[]"); break; + case EVENTUALLY: printf("<>"); break; + case IMPLIES: printf("->"); break; + case EQUIV: printf("<->"); break; + case PREDICATE: printf("predicate"); break; + case OR: printf("||"); break; + case AND: printf("&&"); break; + case NOT: printf("!"); break; + case U_OPER: printf("U"); break; + case V_OPER: printf("V"); break; +#ifdef NXT + case NEXT: printf("X"); break; +#endif + case TRUE: printf("true"); break; + case FALSE: printf("false"); break; + case ';': printf("end of formula"); break; + default: printf("%c", n); break; + } +} + +static void +non_fatal(char *s1, char *s2) +{ extern int tl_yychar; + int i; + + printf("ltl2ba: "); + if (s2) + printf(s1, s2); + else + printf(s1); + if (tl_yychar != -1 && tl_yychar != 0) + { printf(", saw '"); + tl_explain(tl_yychar); + printf("'"); + } + printf("\nltl2ba: %s\n---------", uform); + for (i = 0; i < cnt; i++) + printf("-"); + printf("^\n"); + fflush(stdout); + tl_errs++; +} + +void +tl_yyerror(char *s1) +{ + Fatal(s1, (char *) 0); +} + +void +Fatal(char *s1, char *s2) +{ + non_fatal(s1, s2); + alldone(1); +} + +void +fatal(char *s1, char *s2) +{ + non_fatal(s1, s2); + alldone(1); +} + + diff --git a/mem.c b/mem.c new file mode 100644 index 0000000..d329935 --- /dev/null +++ b/mem.c @@ -0,0 +1,245 @@ +/***** ltl2ba : mem.c *****/ + +/* Written by Denis Oddoux, LIAFA, France */ +/* Copyright (c) 2001 Denis Oddoux */ +/* Modified by Paul Gastin, LSV, France */ +/* Copyright (c) 2007 Paul Gastin */ +/* */ +/* 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., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA*/ +/* */ +/* Based on the translation algorithm by Gastin and Oddoux, */ +/* presented at the 13th International Conference on Computer Aided */ +/* Verification, CAV 2001, Paris, France. */ +/* Proceedings - LNCS 2102, pp. 53-65 */ +/* */ +/* Send bug-reports and/or questions to Paul Gastin */ +/* http://www.lsv.ens-cachan.fr/~gastin */ +/* */ +/* Some of the code in this file was taken from the Spin software */ +/* Written by Gerard J. Holzmann, Bell Laboratories, U.S.A. */ + +#include "ltl2ba.h" + +#if 1 +#define log(e, u, d) event[e][(int) u] += (long) d; +#else +#define log(e, u, d) +#endif + +#define A_LARGE 80 +#define A_USER 0x55000000 +#define NOTOOBIG 32768 + +#define POOL 0 +#define ALLOC 1 +#define FREE 2 +#define NREVENT 3 + +extern unsigned long All_Mem; +extern int tl_verbose; + +ATrans *atrans_list = (ATrans *)0; +GTrans *gtrans_list = (GTrans *)0; +BTrans *btrans_list = (BTrans *)0; + +int aallocs = 0, afrees = 0, apool = 0; +int gallocs = 0, gfrees = 0, gpool = 0; +int ballocs = 0, bfrees = 0, bpool = 0; + +union M { + long size; + union M *link; +}; + +static union M *freelist[A_LARGE]; +static long req[A_LARGE]; +static long event[NREVENT][A_LARGE]; + +void * +tl_emalloc(int U) +{ union M *m; + long r, u; + void *rp; + + u = (long) ((U-1)/sizeof(union M) + 2); + + if (u >= A_LARGE) + { log(ALLOC, 0, 1); + if (tl_verbose) + printf("tl_spin: memalloc %ld bytes\n", u); + m = (union M *) emalloc((int) u*sizeof(union M)); + All_Mem += (unsigned long) u*sizeof(union M); + } else + { if (!freelist[u]) + { r = req[u] += req[u] ? req[u] : 1; + if (r >= NOTOOBIG) + r = req[u] = NOTOOBIG; + log(POOL, u, r); + freelist[u] = (union M *) + emalloc((int) r*u*sizeof(union M)); + All_Mem += (unsigned long) r*u*sizeof(union M); + m = freelist[u] + (r-2)*u; + for ( ; m >= freelist[u]; m -= u) + m->link = m+u; + } + log(ALLOC, u, 1); + m = freelist[u]; + freelist[u] = m->link; + } + m->size = (u|A_USER); + + for (r = 1; r < u; ) + (&m->size)[r++] = 0; + + rp = (void *) (m+1); + memset(rp, 0, U); + return rp; +} + +void +tfree(void *v) +{ union M *m = (union M *) v; + long u; + + --m; + if ((m->size&0xFF000000) != A_USER) + Fatal("releasing a free block", (char *)0); + + u = (m->size &= 0xFFFFFF); + if (u >= A_LARGE) + { log(FREE, 0, 1); + /* free(m); */ + } else + { log(FREE, u, 1); + m->link = freelist[u]; + freelist[u] = m; + } +} + +ATrans* emalloc_atrans() { + ATrans *result; + if(!atrans_list) { + result = (ATrans *)tl_emalloc(sizeof(GTrans)); + result->pos = new_set(1); + result->neg = new_set(1); + result->to = new_set(0); + apool++; + } + else { + result = atrans_list; + atrans_list = atrans_list->nxt; + result->nxt = (ATrans *)0; + } + aallocs++; + return result; +} + +void free_atrans(ATrans *t, int rec) { + if(!t) return; + if(rec) free_atrans(t->nxt, rec); + t->nxt = atrans_list; + atrans_list = t; + afrees++; +} + +void free_all_atrans() { + ATrans *t; + while(atrans_list) { + t = atrans_list; + atrans_list = t->nxt; + tfree(t->to); + tfree(t->pos); + tfree(t->neg); + tfree(t); + } +} + +GTrans* emalloc_gtrans() { + GTrans *result; + if(!gtrans_list) { + result = (GTrans *)tl_emalloc(sizeof(GTrans)); + result->pos = new_set(1); + result->neg = new_set(1); + result->final = new_set(0); + gpool++; + } + else { + result = gtrans_list; + gtrans_list = gtrans_list->nxt; + } + gallocs++; + return result; +} + +void free_gtrans(GTrans *t, GTrans *sentinel, int fly) { + gfrees++; + if(sentinel && (t != sentinel)) { + free_gtrans(t->nxt, sentinel, fly); + if(fly) t->to->incoming--; + } + t->nxt = gtrans_list; + gtrans_list = t; +} + +BTrans* emalloc_btrans() { + BTrans *result; + if(!btrans_list) { + result = (BTrans *)tl_emalloc(sizeof(BTrans)); + result->pos = new_set(1); + result->neg = new_set(1); + bpool++; + } + else { + result = btrans_list; + btrans_list = btrans_list->nxt; + } + ballocs++; + return result; +} + +void free_btrans(BTrans *t, BTrans *sentinel, int fly) { + bfrees++; + if(sentinel && (t != sentinel)) { + free_btrans(t->nxt, sentinel, fly); + if(fly) t->to->incoming--; + } + t->nxt = btrans_list; + btrans_list = t; +} + +void +a_stats(void) +{ long p, a, f; + int i; + + printf(" size\t pool\tallocs\t frees\n"); + + for (i = 0; i < A_LARGE; i++) + { p = event[POOL][i]; + a = event[ALLOC][i]; + f = event[FREE][i]; + + if(p|a|f) + printf("%5d\t%6ld\t%6ld\t%6ld\n", + i, p, a, f); + } + + printf("atrans\t%6d\t%6d\t%6d\n", + apool, aallocs, afrees); + printf("gtrans\t%6d\t%6d\t%6d\n", + gpool, gallocs, gfrees); + printf("btrans\t%6d\t%6d\t%6d\n", + bpool, ballocs, bfrees); +} diff --git a/parse.c b/parse.c new file mode 100644 index 0000000..ebcf82c --- /dev/null +++ b/parse.c @@ -0,0 +1,572 @@ +/***** ltl2ba : parse.c *****/ + +/* Written by Denis Oddoux, LIAFA, France */ +/* Copyright (c) 2001 Denis Oddoux */ +/* Modified by Paul Gastin, LSV, France */ +/* Copyright (c) 2007 Paul Gastin */ +/* */ +/* 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., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA*/ +/* */ +/* Based on the translation algorithm by Gastin and Oddoux, */ +/* presented at the 13th International Conference on Computer Aided */ +/* Verification, CAV 2001, Paris, France. */ +/* Proceedings - LNCS 2102, pp. 53-65 */ +/* */ +/* Send bug-reports and/or questions to Paul Gastin */ +/* http://www.lsv.ens-cachan.fr/~gastin */ +/* */ +/* Some of the code in this file was taken from the Spin software */ +/* Written by Gerard J. Holzmann, Bell Laboratories, U.S.A. */ + +#include "ltl2ba.h" + +extern int tl_yylex(void); +extern int tl_verbose, tl_simp_log; + +int tl_yychar = 0; +YYSTYPE tl_yylval; + +static Node *tl_formula(void); +static Node *tl_factor(void); +static Node *tl_level(int); + +static int prec[2][4] = { + { U_OPER, V_OPER, 0, 0}, /* left associative */ + { OR, AND, IMPLIES, EQUIV, }, /* left associative */ +}; + +static int +implies(Node *a, Node *b) +{ + return + (isequal(a,b) || + b->ntyp == TRUE || + a->ntyp == FALSE || + (b->ntyp == AND && implies(a, b->lft) && implies(a, b->rgt)) || + (a->ntyp == OR && implies(a->lft, b) && implies(a->rgt, b)) || + (a->ntyp == AND && (implies(a->lft, b) || implies(a->rgt, b))) || + (b->ntyp == OR && (implies(a, b->lft) || implies(a, b->rgt))) || + (b->ntyp == U_OPER && implies(a, b->rgt)) || + (a->ntyp == V_OPER && implies(a->rgt, b)) || + (a->ntyp == U_OPER && implies(a->lft, b) && implies(a->rgt, b)) || + (b->ntyp == V_OPER && implies(a, b->lft) && implies(a, b->rgt)) || + ((a->ntyp == U_OPER || a->ntyp == V_OPER) && a->ntyp == b->ntyp && + implies(a->lft, b->lft) && implies(a->rgt, b->rgt))); +} + +static Node * +bin_simpler(Node *ptr) +{ Node *a, *b; + + if (ptr) + switch (ptr->ntyp) { + case U_OPER: + if (ptr->rgt->ntyp == TRUE + || ptr->rgt->ntyp == FALSE + || ptr->lft->ntyp == FALSE) + { ptr = ptr->rgt; + break; + } + if (implies(ptr->lft, ptr->rgt)) /* NEW */ + { ptr = ptr->rgt; + break; + } + if (ptr->lft->ntyp == U_OPER + && isequal(ptr->lft->lft, ptr->rgt)) + { /* (p U q) U p = (q U p) */ + ptr->lft = ptr->lft->rgt; + break; + } + if (ptr->rgt->ntyp == U_OPER + && implies(ptr->lft, ptr->rgt->lft)) + { /* NEW */ + ptr = ptr->rgt; + break; + } +#ifdef NXT + /* X p U X q == X (p U q) */ + if (ptr->rgt->ntyp == NEXT + && ptr->lft->ntyp == NEXT) + { ptr = tl_nn(NEXT, + tl_nn(U_OPER, + ptr->lft->lft, + ptr->rgt->lft), ZN); + break; + } + + /* NEW : F X p == X F p */ + if (ptr->lft->ntyp == TRUE && + ptr->rgt->ntyp == NEXT) { + ptr = tl_nn(NEXT, tl_nn(U_OPER, True, ptr->rgt->lft), ZN); + break; + } + +#endif + + /* NEW : F G F p == G F p */ + if (ptr->lft->ntyp == TRUE && + ptr->rgt->ntyp == V_OPER && + ptr->rgt->lft->ntyp == FALSE && + ptr->rgt->rgt->ntyp == U_OPER && + ptr->rgt->rgt->lft->ntyp == TRUE) { + ptr = ptr->rgt; + break; + } + + /* NEW */ + if (ptr->lft->ntyp != TRUE && + implies(push_negation(tl_nn(NOT, dupnode(ptr->rgt), ZN)), + ptr->lft)) + { ptr->lft = True; + break; + } + break; + case V_OPER: + if (ptr->rgt->ntyp == FALSE + || ptr->rgt->ntyp == TRUE + || ptr->lft->ntyp == TRUE) + { ptr = ptr->rgt; + break; + } + if (implies(ptr->rgt, ptr->lft)) + { /* p V p = p */ + ptr = ptr->rgt; + break; + } + /* F V (p V q) == F V q */ + if (ptr->lft->ntyp == FALSE + && ptr->rgt->ntyp == V_OPER) + { ptr->rgt = ptr->rgt->rgt; + break; + } +#ifdef NXT + /* NEW : G X p == X G p */ + if (ptr->lft->ntyp == FALSE && + ptr->rgt->ntyp == NEXT) { + ptr = tl_nn(NEXT, tl_nn(V_OPER, False, ptr->rgt->lft), ZN); + break; + } +#endif + /* NEW : G F G p == F G p */ + if (ptr->lft->ntyp == FALSE && + ptr->rgt->ntyp == U_OPER && + ptr->rgt->lft->ntyp == TRUE && + ptr->rgt->rgt->ntyp == V_OPER && + ptr->rgt->rgt->lft->ntyp == FALSE) { + ptr = ptr->rgt; + break; + } + + /* NEW */ + if (ptr->rgt->ntyp == V_OPER + && implies(ptr->rgt->lft, ptr->lft)) + { ptr = ptr->rgt; + break; + } + + /* NEW */ + if (ptr->lft->ntyp != FALSE && + implies(ptr->lft, + push_negation(tl_nn(NOT, dupnode(ptr->rgt), ZN)))) + { ptr->lft = False; + break; + } + break; +#ifdef NXT + case NEXT: + /* NEW : X G F p == G F p */ + if (ptr->lft->ntyp == V_OPER && + ptr->lft->lft->ntyp == FALSE && + ptr->lft->rgt->ntyp == U_OPER && + ptr->lft->rgt->lft->ntyp == TRUE) { + ptr = ptr->lft; + break; + } + /* NEW : X F G p == F G p */ + if (ptr->lft->ntyp == U_OPER && + ptr->lft->lft->ntyp == TRUE && + ptr->lft->rgt->ntyp == V_OPER && + ptr->lft->rgt->lft->ntyp == FALSE) { + ptr = ptr->lft; + break; + } + break; +#endif + case IMPLIES: + if (implies(ptr->lft, ptr->rgt)) + { ptr = True; + break; + } + ptr = tl_nn(OR, Not(ptr->lft), ptr->rgt); + ptr = rewrite(ptr); + break; + case EQUIV: + if (implies(ptr->lft, ptr->rgt) && + implies(ptr->rgt, ptr->lft)) + { ptr = True; + break; + } + a = rewrite(tl_nn(AND, + dupnode(ptr->lft), + dupnode(ptr->rgt))); + b = rewrite(tl_nn(AND, + Not(ptr->lft), + Not(ptr->rgt))); + ptr = tl_nn(OR, a, b); + ptr = rewrite(ptr); + break; + case AND: + /* p && (q U p) = p */ + if (ptr->rgt->ntyp == U_OPER + && isequal(ptr->rgt->rgt, ptr->lft)) + { ptr = ptr->lft; + break; + } + if (ptr->lft->ntyp == U_OPER + && isequal(ptr->lft->rgt, ptr->rgt)) + { ptr = ptr->rgt; + break; + } + + /* p && (q V p) == q V p */ + if (ptr->rgt->ntyp == V_OPER + && isequal(ptr->rgt->rgt, ptr->lft)) + { ptr = ptr->rgt; + break; + } + if (ptr->lft->ntyp == V_OPER + && isequal(ptr->lft->rgt, ptr->rgt)) + { ptr = ptr->lft; + break; + } + + /* (p U q) && (r U q) = (p && r) U q*/ + if (ptr->rgt->ntyp == U_OPER + && ptr->lft->ntyp == U_OPER + && isequal(ptr->rgt->rgt, ptr->lft->rgt)) + { ptr = tl_nn(U_OPER, + tl_nn(AND, ptr->lft->lft, ptr->rgt->lft), + ptr->lft->rgt); + break; + } + + /* (p V q) && (p V r) = p V (q && r) */ + if (ptr->rgt->ntyp == V_OPER + && ptr->lft->ntyp == V_OPER + && isequal(ptr->rgt->lft, ptr->lft->lft)) + { ptr = tl_nn(V_OPER, + ptr->rgt->lft, + tl_nn(AND, ptr->lft->rgt, ptr->rgt->rgt)); + break; + } +#ifdef NXT + /* X p && X q == X (p && q) */ + if (ptr->rgt->ntyp == NEXT + && ptr->lft->ntyp == NEXT) + { ptr = tl_nn(NEXT, + tl_nn(AND, + ptr->rgt->lft, + ptr->lft->lft), ZN); + break; + } +#endif + + /* (p V q) && (r U q) == p V q */ + if (ptr->rgt->ntyp == U_OPER + && ptr->lft->ntyp == V_OPER + && isequal(ptr->lft->rgt, ptr->rgt->rgt)) + { ptr = ptr->lft; + break; + } + + if (isequal(ptr->lft, ptr->rgt) /* (p && p) == p */ + || ptr->rgt->ntyp == FALSE /* (p && F) == F */ + || ptr->lft->ntyp == TRUE /* (T && p) == p */ + || implies(ptr->rgt, ptr->lft))/* NEW */ + { ptr = ptr->rgt; + break; + } + if (ptr->rgt->ntyp == TRUE /* (p && T) == p */ + || ptr->lft->ntyp == FALSE /* (F && p) == F */ + || implies(ptr->lft, ptr->rgt))/* NEW */ + { ptr = ptr->lft; + break; + } + + /* NEW : F G p && F G q == F G (p && q) */ + if (ptr->lft->ntyp == U_OPER && + ptr->lft->lft->ntyp == TRUE && + ptr->lft->rgt->ntyp == V_OPER && + ptr->lft->rgt->lft->ntyp == FALSE && + ptr->rgt->ntyp == U_OPER && + ptr->rgt->lft->ntyp == TRUE && + ptr->rgt->rgt->ntyp == V_OPER && + ptr->rgt->rgt->lft->ntyp == FALSE) + { + ptr = tl_nn(U_OPER, True, + tl_nn(V_OPER, False, + tl_nn(AND, ptr->lft->rgt->rgt, + ptr->rgt->rgt->rgt))); + break; + } + + /* NEW */ + if (implies(ptr->lft, + push_negation(tl_nn(NOT, dupnode(ptr->rgt), ZN))) + || implies(ptr->rgt, + push_negation(tl_nn(NOT, dupnode(ptr->lft), ZN)))) + { ptr = False; + break; + } + break; + + case OR: + /* p || (q U p) == q U p */ + if (ptr->rgt->ntyp == U_OPER + && isequal(ptr->rgt->rgt, ptr->lft)) + { ptr = ptr->rgt; + break; + } + + /* p || (q V p) == p */ + if (ptr->rgt->ntyp == V_OPER + && isequal(ptr->rgt->rgt, ptr->lft)) + { ptr = ptr->lft; + break; + } + + /* (p U q) || (p U r) = p U (q || r) */ + if (ptr->rgt->ntyp == U_OPER + && ptr->lft->ntyp == U_OPER + && isequal(ptr->rgt->lft, ptr->lft->lft)) + { ptr = tl_nn(U_OPER, + ptr->rgt->lft, + tl_nn(OR, ptr->lft->rgt, ptr->rgt->rgt)); + break; + } + + if (isequal(ptr->lft, ptr->rgt) /* (p || p) == p */ + || ptr->rgt->ntyp == FALSE /* (p || F) == p */ + || ptr->lft->ntyp == TRUE /* (T || p) == T */ + || implies(ptr->rgt, ptr->lft))/* NEW */ + { ptr = ptr->lft; + break; + } + if (ptr->rgt->ntyp == TRUE /* (p || T) == T */ + || ptr->lft->ntyp == FALSE /* (F || p) == p */ + || implies(ptr->lft, ptr->rgt))/* NEW */ + { ptr = ptr->rgt; + break; + } + + /* (p V q) || (r V q) = (p || r) V q */ + if (ptr->rgt->ntyp == V_OPER + && ptr->lft->ntyp == V_OPER + && isequal(ptr->lft->rgt, ptr->rgt->rgt)) + { ptr = tl_nn(V_OPER, + tl_nn(OR, ptr->lft->lft, ptr->rgt->lft), + ptr->rgt->rgt); + break; + } + + /* (p V q) || (r U q) == r U q */ + if (ptr->rgt->ntyp == U_OPER + && ptr->lft->ntyp == V_OPER + && isequal(ptr->lft->rgt, ptr->rgt->rgt)) + { ptr = ptr->rgt; + break; + } + + /* NEW : G F p || G F q == G F (p || q) */ + if (ptr->lft->ntyp == V_OPER && + ptr->lft->lft->ntyp == FALSE && + ptr->lft->rgt->ntyp == U_OPER && + ptr->lft->rgt->lft->ntyp == TRUE && + ptr->rgt->ntyp == V_OPER && + ptr->rgt->lft->ntyp == FALSE && + ptr->rgt->rgt->ntyp == U_OPER && + ptr->rgt->rgt->lft->ntyp == TRUE) + { + ptr = tl_nn(V_OPER, False, + tl_nn(U_OPER, True, + tl_nn(OR, ptr->lft->rgt->rgt, + ptr->rgt->rgt->rgt))); + break; + } + + /* NEW */ + if (implies(push_negation(tl_nn(NOT, dupnode(ptr->rgt), ZN)), + ptr->lft) + || implies(push_negation(tl_nn(NOT, dupnode(ptr->lft), ZN)), + ptr->rgt)) + { ptr = True; + break; + } + break; + } + return ptr; +} + +static Node * +bin_minimal(Node *ptr) +{ if (ptr) + switch (ptr->ntyp) { + case IMPLIES: + return tl_nn(OR, Not(ptr->lft), ptr->rgt); + case EQUIV: + return tl_nn(OR, + tl_nn(AND,dupnode(ptr->lft),dupnode(ptr->rgt)), + tl_nn(AND,Not(ptr->lft),Not(ptr->rgt))); + } + return ptr; +} + +static Node * +tl_factor(void) +{ Node *ptr = ZN; + + switch (tl_yychar) { + case '(': + ptr = tl_formula(); + if (tl_yychar != ')') + tl_yyerror("expected ')'"); + tl_yychar = tl_yylex(); + goto simpl; + case NOT: + ptr = tl_yylval; + tl_yychar = tl_yylex(); + ptr->lft = tl_factor(); + ptr = push_negation(ptr); + goto simpl; + case ALWAYS: + tl_yychar = tl_yylex(); + + ptr = tl_factor(); + + if(tl_simp_log) { + if (ptr->ntyp == FALSE + || ptr->ntyp == TRUE) + break; /* [] false == false */ + + if (ptr->ntyp == V_OPER) + { if (ptr->lft->ntyp == FALSE) + break; /* [][]p = []p */ + + ptr = ptr->rgt; /* [] (p V q) = [] q */ + } + } + + ptr = tl_nn(V_OPER, False, ptr); + goto simpl; +#ifdef NXT + case NEXT: + tl_yychar = tl_yylex(); + + ptr = tl_factor(); + + if ((ptr->ntyp == TRUE || ptr->ntyp == FALSE)&& tl_simp_log) + break; /* X true = true , X false = false */ + + ptr = tl_nn(NEXT, ptr, ZN); + goto simpl; +#endif + case EVENTUALLY: + tl_yychar = tl_yylex(); + + ptr = tl_factor(); + + if(tl_simp_log) { + if (ptr->ntyp == TRUE + || ptr->ntyp == FALSE) + break; /* <> true == true */ + + if (ptr->ntyp == U_OPER + && ptr->lft->ntyp == TRUE) + break; /* <><>p = <>p */ + + if (ptr->ntyp == U_OPER) + { /* <> (p U q) = <> q */ + ptr = ptr->rgt; + /* fall thru */ + } + } + + ptr = tl_nn(U_OPER, True, ptr); + simpl: + if (tl_simp_log) + ptr = bin_simpler(ptr); + break; + case PREDICATE: + ptr = tl_yylval; + tl_yychar = tl_yylex(); + break; + case TRUE: + case FALSE: + ptr = tl_yylval; + tl_yychar = tl_yylex(); + break; + } + if (!ptr) tl_yyerror("expected predicate"); +#if 0 + printf("factor: "); + tl_explain(ptr->ntyp); + printf("\n"); +#endif + return ptr; +} + +static Node * +tl_level(int nr) +{ int i; Node *ptr = ZN; + + if (nr < 0) + return tl_factor(); + + ptr = tl_level(nr-1); +again: + for (i = 0; i < 4; i++) + if (tl_yychar == prec[nr][i]) + { tl_yychar = tl_yylex(); + ptr = tl_nn(prec[nr][i], + ptr, tl_level(nr-1)); + if(tl_simp_log) ptr = bin_simpler(ptr); + else ptr = bin_minimal(ptr); + goto again; + } + if (!ptr) tl_yyerror("syntax error"); +#if 0 + printf("level %d: ", nr); + tl_explain(ptr->ntyp); + printf("\n"); +#endif + return ptr; +} + +static Node * +tl_formula(void) +{ tl_yychar = tl_yylex(); + return tl_level(1); /* 2 precedence levels, 1 and 0 */ +} + +void +tl_parse(void) +{ Node *n = tl_formula(); + if (tl_verbose) + { printf("formula: "); + put_uform(); + printf("\n"); + } + trans(n); +} diff --git a/rewrt.c b/rewrt.c new file mode 100644 index 0000000..2b69ab7 --- /dev/null +++ b/rewrt.c @@ -0,0 +1,326 @@ +/***** ltl2ba : rewrt.c *****/ + +/* Written by Denis Oddoux, LIAFA, France */ +/* Copyright (c) 2001 Denis Oddoux */ +/* Modified by Paul Gastin, LSV, France */ +/* Copyright (c) 2007 Paul Gastin */ +/* */ +/* 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., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA*/ +/* */ +/* Based on the translation algorithm by Gastin and Oddoux, */ +/* presented at the 13th International Conference on Computer Aided */ +/* Verification, CAV 2001, Paris, France. */ +/* Proceedings - LNCS 2102, pp. 53-65 */ +/* */ +/* Send bug-reports and/or questions to Paul Gastin */ +/* http://www.lsv.ens-cachan.fr/~gastin */ +/* */ +/* Some of the code in this file was taken from the Spin software */ +/* Written by Gerard J. Holzmann, Bell Laboratories, U.S.A. */ + +#include "ltl2ba.h" + +extern int tl_verbose; + +static Node *can = ZN; + +Node * +right_linked(Node *n) +{ + if (!n) return n; + + if (n->ntyp == AND || n->ntyp == OR) + while (n->lft && n->lft->ntyp == n->ntyp) + { Node *tmp = n->lft; + n->lft = tmp->rgt; + tmp->rgt = n; + n = tmp; + } + + n->lft = right_linked(n->lft); + n->rgt = right_linked(n->rgt); + + return n; +} + +Node * +canonical(Node *n) +{ Node *m; /* assumes input is right_linked */ + + if (!n) return n; + if (m = in_cache(n)) + return m; + + n->rgt = canonical(n->rgt); + n->lft = canonical(n->lft); + + return cached(n); +} + +Node * +push_negation(Node *n) +{ Node *m; + + Assert(n->ntyp == NOT, n->ntyp); + + switch (n->lft->ntyp) { + case TRUE: + releasenode(0, n->lft); + n->lft = ZN; + n->ntyp = FALSE; + break; + case FALSE: + releasenode(0, n->lft); + n->lft = ZN; + n->ntyp = TRUE; + break; + case NOT: + m = n->lft->lft; + releasenode(0, n->lft); + n->lft = ZN; + releasenode(0, n); + n = m; + break; + case V_OPER: + n->ntyp = U_OPER; + goto same; + case U_OPER: + n->ntyp = V_OPER; + goto same; +#ifdef NXT + case NEXT: + n->ntyp = NEXT; + n->lft->ntyp = NOT; + n->lft = push_negation(n->lft); + break; +#endif + case AND: + n->ntyp = OR; + goto same; + case OR: + n->ntyp = AND; + +same: m = n->lft->rgt; + n->lft->rgt = ZN; + + n->rgt = Not(m); + n->lft->ntyp = NOT; + m = n->lft; + n->lft = push_negation(m); + break; + } + + return rewrite(n); +} + +static void +addcan(int tok, Node *n) +{ Node *m, *prev = ZN; + Node **ptr; + Node *N; + Symbol *s, *t; int cmp; + + if (!n) return; + + if (n->ntyp == tok) + { addcan(tok, n->rgt); + addcan(tok, n->lft); + return; + } +#if 0 + if ((tok == AND && n->ntyp == TRUE) + || (tok == OR && n->ntyp == FALSE)) + return; +#endif + N = dupnode(n); + if (!can) + { can = N; + return; + } + + s = DoDump(N); + if (can->ntyp != tok) /* only one element in list so far */ + { ptr = &can; + goto insert; + } + + /* there are at least 2 elements in list */ + prev = ZN; + for (m = can; m->ntyp == tok && m->rgt; prev = m, m = m->rgt) + { t = DoDump(m->lft); + cmp = strcmp(s->name, t->name); + if (cmp == 0) /* duplicate */ + return; + if (cmp < 0) + { if (!prev) + { can = tl_nn(tok, N, can); + return; + } else + { ptr = &(prev->rgt); + goto insert; + } } } + + /* new entry goes at the end of the list */ + ptr = &(prev->rgt); +insert: + t = DoDump(*ptr); + cmp = strcmp(s->name, t->name); + if (cmp == 0) /* duplicate */ + return; + if (cmp < 0) + *ptr = tl_nn(tok, N, *ptr); + else + *ptr = tl_nn(tok, *ptr, N); +} + +static void +marknode(int tok, Node *m) +{ + if (m->ntyp != tok) + { releasenode(0, m->rgt); + m->rgt = ZN; + } + m->ntyp = -1; +} + +Node * +Canonical(Node *n) +{ Node *m, *p, *k1, *k2, *prev, *dflt = ZN; + int tok; + + if (!n) return n; + + tok = n->ntyp; + if (tok != AND && tok != OR) + return n; + + can = ZN; + addcan(tok, n); +#if 1 + Debug("\nA0: "); Dump(can); + Debug("\nA1: "); Dump(n); Debug("\n"); +#endif + releasenode(1, n); + + /* mark redundant nodes */ + if (tok == AND) + { for (m = can; m; m = (m->ntyp == AND) ? m->rgt : ZN) + { k1 = (m->ntyp == AND) ? m->lft : m; + if (k1->ntyp == TRUE) + { marknode(AND, m); + dflt = True; + continue; + } + if (k1->ntyp == FALSE) + { releasenode(1, can); + can = False; + goto out; + } } + for (m = can; m; m = (m->ntyp == AND) ? m->rgt : ZN) + for (p = can; p; p = (p->ntyp == AND) ? p->rgt : ZN) + { if (p == m + || p->ntyp == -1 + || m->ntyp == -1) + continue; + k1 = (m->ntyp == AND) ? m->lft : m; + k2 = (p->ntyp == AND) ? p->lft : p; + + if (isequal(k1, k2)) + { marknode(AND, p); + continue; + } + if (anywhere(OR, k1, k2)) + { marknode(AND, p); + continue; + } + if (k2->ntyp == U_OPER + && anywhere(AND, k2->rgt, can)) + { marknode(AND, p); + continue; + } /* q && (p U q) = q */ + } } + if (tok == OR) + { for (m = can; m; m = (m->ntyp == OR) ? m->rgt : ZN) + { k1 = (m->ntyp == OR) ? m->lft : m; + if (k1->ntyp == FALSE) + { marknode(OR, m); + dflt = False; + continue; + } + if (k1->ntyp == TRUE) + { releasenode(1, can); + can = True; + goto out; + } } + for (m = can; m; m = (m->ntyp == OR) ? m->rgt : ZN) + for (p = can; p; p = (p->ntyp == OR) ? p->rgt : ZN) + { if (p == m + || p->ntyp == -1 + || m->ntyp == -1) + continue; + k1 = (m->ntyp == OR) ? m->lft : m; + k2 = (p->ntyp == OR) ? p->lft : p; + + if (isequal(k1, k2)) + { marknode(OR, p); + continue; + } + if (anywhere(AND, k1, k2)) + { marknode(OR, p); + continue; + } + if (k2->ntyp == V_OPER + && k2->lft->ntyp == FALSE + && anywhere(AND, k2->rgt, can)) + { marknode(OR, p); + continue; + } /* p || (F V p) = p */ + } } + for (m = can, prev = ZN; m; ) /* remove marked nodes */ + { if (m->ntyp == -1) + { k2 = m->rgt; + releasenode(0, m); + if (!prev) + { m = can = can->rgt; + } else + { m = prev->rgt = k2; + /* if deleted the last node in a chain */ + if (!prev->rgt && prev->lft + && (prev->ntyp == AND || prev->ntyp == OR)) + { k1 = prev->lft; + prev->ntyp = prev->lft->ntyp; + prev->sym = prev->lft->sym; + prev->rgt = prev->lft->rgt; + prev->lft = prev->lft->lft; + releasenode(0, k1); + } + } + continue; + } + prev = m; + m = m->rgt; + } +out: +#if 1 + Debug("A2: "); Dump(can); Debug("\n"); +#endif + if (!can) + { if (!dflt) + fatal("cannot happen, Canonical", (char *) 0); + return dflt; + } + + return can; +} diff --git a/set.c b/set.c new file mode 100644 index 0000000..2fdaff9 --- /dev/null +++ b/set.c @@ -0,0 +1,209 @@ +/***** ltl2ba : set.c *****/ + +/* Written by Denis Oddoux, LIAFA, France */ +/* Copyright (c) 2001 Denis Oddoux */ +/* Modified by Paul Gastin, LSV, France */ +/* Copyright (c) 2007 Paul Gastin */ +/* */ +/* 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., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA*/ +/* */ +/* Based on the translation algorithm by Gastin and Oddoux, */ +/* presented at the 13th International Conference on Computer Aided */ +/* Verification, CAV 2001, Paris, France. */ +/* Proceedings - LNCS 2102, pp. 53-65 */ +/* */ +/* Send bug-reports and/or questions to Paul Gastin */ +/* http://www.lsv.ens-cachan.fr/~gastin */ + +#include "ltl2ba.h" + +extern FILE *tl_out; +extern int node_size, sym_size, scc_size; +extern char **sym_table; + +int mod = 8 * sizeof(int); + + +/* type = 2 for scc set, 1 for symbol sets, 0 for nodes sets */ + +#define set_size(t) (t==1?sym_size:(t==2?scc_size:node_size)) + +int *new_set(int type) /* creates a new set */ +{ + return (int *)tl_emalloc(set_size(type) * sizeof(int)); +} + +int *clear_set(int *l, int type) /* clears the set */ +{ + int i; + for(i = 0; i < set_size(type); i++) { + l[i] = 0; + } + return l; +} + +int *make_set(int n, int type) /* creates the set {n}, or the empty set if n = -1 */ +{ + int *l = clear_set(new_set(type), type); + if(n == -1) return l; + l[n/mod] = 1 << (n%mod); + return l; +} + +void copy_set(int *from, int *to, int type) /* copies a set */ +{ + int i; + for(i = 0; i < set_size(type); i++) + to[i] = from[i]; +} + +int *dup_set(int *l, int type) /* duplicates a set */ +{ + int i, *m = new_set(type); + for(i = 0; i < set_size(type); i++) + m[i] = l[i]; + return m; +} + +void merge_sets(int *l1, int *l2, int type) /* puts the union of the two sets in l1 */ +{ + int i; + for(i = 0; i < set_size(type); i++) + l1[i] = l1[i] | l2[i]; +} + +void do_merge_sets(int *l, int *l1, int *l2, int type) /* makes the union of two sets */ +{ + int i; + for(i = 0; i < set_size(type); i++) + l[i] = l1[i] | l2[i]; +} + +int *intersect_sets(int *l1, int *l2, int type) /* makes the intersection of two sets */ +{ + int i, *l = new_set(type); + for(i = 0; i < set_size(type); i++) + l[i] = l1[i] & l2[i]; + return l; +} + +int empty_intersect_sets(int *l1, int *l2, int type) /* tests intersection of two sets */ +{ + int i, test = 0; + for(i = 0; i < set_size(type); i++) + test |= l1[i] & l2[i]; + return !test; +} + +void add_set(int *l, int n) /* adds an element to a set */ +{ + l[n/mod] |= 1 << (n%mod); +} + +void rem_set(int *l, int n) /* removes an element from a set */ +{ + l[n/mod] &= (-1 - (1 << (n%mod))); +} + +void spin_print_set(int *pos, int *neg) /* prints the content of a set for spin */ +{ + int i, j, start = 1; + for(i = 0; i < sym_size; i++) + for(j = 0; j < mod; j++) { + if(pos[i] & (1 << j)) { + if(!start) + fprintf(tl_out, " && "); + fprintf(tl_out, "%s", sym_table[mod * i + j]); + start = 0; + } + if(neg[i] & (1 << j)) { + if(!start) + fprintf(tl_out, " && "); + fprintf(tl_out, "!%s", sym_table[mod * i + j]); + start = 0; + } + } + if(start) + fprintf(tl_out, "1"); +} + +void print_set(int *l, int type) /* prints the content of a set */ +{ + int i, j, start = 1;; + if(type != 1) fprintf(tl_out, "{"); + for(i = 0; i < set_size(type); i++) + for(j = 0; j < mod; j++) + if(l[i] & (1 << j)) { + switch(type) { + case 0: case 2: + if(!start) fprintf(tl_out, ","); + fprintf(tl_out, "%i", mod * i + j); + break; + case 1: + if(!start) fprintf(tl_out, " & "); + fprintf(tl_out, "%s", sym_table[mod * i + j]); + break; + } + start = 0; + } + if(type != 1) fprintf(tl_out, "}"); +} + +int empty_set(int *l, int type) /* tests if a set is the empty set */ +{ + int i, test = 0; + for(i = 0; i < set_size(type); i++) + test |= l[i]; + return !test; +} + +int same_sets(int *l1, int *l2, int type) /* tests if two sets are identical */ +{ + int i, test = 1; + for(i = 0; i < set_size(type); i++) + test &= (l1[i] == l2[i]); + return test; +} + +int included_set(int *l1, int *l2, int type) +{ /* tests if the first set is included in the second one */ + int i, test = 0; + for(i = 0; i < set_size(type); i++) + test |= (l1[i] & ~l2[i]); + return !test; +} + +int in_set(int *l, int n) /* tests if an element is in a set */ +{ + return(l[n/mod] & (1 << (n%mod))); +} + +int *list_set(int *l, int type) /* transforms a set into a list */ +{ + int i, j, size = 1, *list; + for(i = 0; i < set_size(type); i++) + for(j = 0; j < mod; j++) + if(l[i] & (1 << j)) + size++; + list = (int *)tl_emalloc(size * sizeof(int)); + list[0] = size; + size = 1; + for(i = 0; i < set_size(type); i++) + for(j = 0; j < mod; j++) + if(l[i] & (1 << j)) + list[size++] = mod * i + j; + return list; +} + diff --git a/trans.c b/trans.c new file mode 100644 index 0000000..09bdf91 --- /dev/null +++ b/trans.c @@ -0,0 +1,175 @@ +/***** ltl2ba : trans.c *****/ + +/* Written by Denis Oddoux, LIAFA, France */ +/* Copyright (c) 2001 Denis Oddoux */ +/* Modified by Paul Gastin, LSV, France */ +/* Copyright (c) 2007 Paul Gastin */ +/* */ +/* 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., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA*/ +/* */ +/* Based on the translation algorithm by Gastin and Oddoux, */ +/* presented at the 13th International Conference on Computer Aided */ +/* Verification, CAV 2001, Paris, France. */ +/* Proceedings - LNCS 2102, pp. 53-65 */ +/* */ +/* Send bug-reports and/or questions to Paul Gastin */ +/* http://www.lsv.ens-cachan.fr/~gastin */ +/* */ +/* Some of the code in this file was taken from the Spin software */ +/* Written by Gerard J. Holzmann, Bell Laboratories, U.S.A. */ + +#include "ltl2ba.h" + +extern int tl_verbose, tl_terse, tl_errs; +extern FILE *tl_out; + +int Stack_mx=0, Max_Red=0, Total=0; +static char dumpbuf[2048]; + +#ifdef NXT +int +only_nxt(Node *n) +{ + switch (n->ntyp) { + case NEXT: + return 1; + case OR: + case AND: + return only_nxt(n->rgt) && only_nxt(n->lft); + default: + return 0; + } +} +#endif + +int +dump_cond(Node *pp, Node *r, int first) +{ Node *q; + int frst = first; + + if (!pp) return frst; + + q = dupnode(pp); + q = rewrite(q); + + if (q->ntyp == PREDICATE + || q->ntyp == NOT +#ifndef NXT + || q->ntyp == OR +#endif + || q->ntyp == FALSE) + { if (!frst) fprintf(tl_out, " && "); + dump(q); + frst = 0; +#ifdef NXT + } else if (q->ntyp == OR) + { if (!frst) fprintf(tl_out, " && "); + fprintf(tl_out, "(("); + frst = dump_cond(q->lft, r, 1); + + if (!frst) + fprintf(tl_out, ") || ("); + else + { if (only_nxt(q->lft)) + { fprintf(tl_out, "1))"); + return 0; + } + } + + frst = dump_cond(q->rgt, r, 1); + + if (frst) + { if (only_nxt(q->rgt)) + fprintf(tl_out, "1"); + else + fprintf(tl_out, "0"); + frst = 0; + } + + fprintf(tl_out, "))"); +#endif + } else if (q->ntyp == V_OPER + && !anywhere(AND, q->rgt, r)) + { frst = dump_cond(q->rgt, r, frst); + } else if (q->ntyp == AND) + { + frst = dump_cond(q->lft, r, frst); + frst = dump_cond(q->rgt, r, frst); + } + + return frst; +} + +static void +sdump(Node *n) +{ + switch (n->ntyp) { + case PREDICATE: strcat(dumpbuf, n->sym->name); + break; + case U_OPER: strcat(dumpbuf, "U"); + goto common2; + case V_OPER: strcat(dumpbuf, "V"); + goto common2; + case OR: strcat(dumpbuf, "|"); + goto common2; + case AND: strcat(dumpbuf, "&"); +common2: sdump(n->rgt); +common1: sdump(n->lft); + break; +#ifdef NXT + case NEXT: strcat(dumpbuf, "X"); + goto common1; +#endif + case NOT: strcat(dumpbuf, "!"); + goto common1; + case TRUE: strcat(dumpbuf, "T"); + break; + case FALSE: strcat(dumpbuf, "F"); + break; + default: strcat(dumpbuf, "?"); + break; + } +} + +Symbol * +DoDump(Node *n) +{ + if (!n) return ZS; + + if (n->ntyp == PREDICATE) + return n->sym; + + dumpbuf[0] = '\0'; + sdump(n); + return tl_lookup(dumpbuf); +} + +void trans(Node *p) +{ + if (!p || tl_errs) return; + + if (tl_verbose || tl_terse) { + fprintf(tl_out, "\t/* Normlzd: "); + dump(p); + fprintf(tl_out, " */\n"); + } + if (tl_terse) + return; + + mk_alternating(p); + mk_generalized(); + mk_buchi(); +} +