commit be18a22bce449bde5d5e6bb38418aca170e8fd3c Author: Michael Weber Date: Wed Nov 3 23:53:14 2010 +0100 Import ltl2ba-1.1 http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/ 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(); +} +