276 lines
7.4 KiB
C
276 lines
7.4 KiB
C
/***** 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 <stdio.h>
|
|
#include <string.h>
|
|
#include <stdlib.h>
|
|
|
|
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 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();
|
|
|
|
BState* buchi_bstates();
|
|
int buchi_accept();
|
|
|
|
void print_spin_buchi();
|
|
void print_dot_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);
|
|
|
|
#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); } }
|
|
#ifndef min
|
|
# define min(x,y) ((x<y)?x:y)
|
|
#endif
|
|
|
|
/* from main.c */
|
|
extern FILE *tl_out;
|
|
|
|
extern int tl_stats; /* time and size stats */
|
|
extern int tl_simp_log; /* logical simplification */
|
|
extern int tl_simp_diff; /* automata simplification */
|
|
extern int tl_simp_fly; /* on the fly simplification */
|
|
extern int tl_simp_scc; /* use scc simplification */
|
|
extern int tl_fjtofj; /* 2eme fj */
|
|
extern int tl_errs;
|
|
extern int tl_verbose;
|
|
extern int tl_terse;
|
|
extern unsigned long All_Mem;
|
|
|
|
extern int (*tl_yylex)(); /* hook for lexer */
|
|
|
|
int ltl2ba_init();
|
|
int set_uform(const char *str);
|
|
void append_uform(const char *str);
|
|
void put_uform();
|
|
void alldone(int status);
|
|
|