Commit f986550d authored by Christian Müller's avatar Christian Müller
Browse files

aalta

parent e57b83c3
FORMULAFILES = formula/aalta_formula.cpp formula/dnf_clause.cpp \
formula/dnf_formula.cpp formula/olg_formula.cpp formula/olg_item.cpp
PARSERFILES = ltlparser/ltl_formula.c ltlparser/ltllexer.c ltlparser/ltlparser.c ltlparser/trans.c
UTILFILES = util/utility.cpp
BUCHI = buchi/buchi_node.cpp buchi/buchi_automata.cpp
MINISAT = minisat/core/Solver.cc
CHECKING = checking/checker.cpp checking/nondeter_checker.cpp checking/scc.cpp
PROGRESSION = progression/nondeter_prog_state.cpp
ALLFILES = $(CHECKING) $(PROGRESSION) $(MINISAT) $(FORMULAFILES) $(PARSERFILES) $(UTILFILES) $(BUCHI) sat_solver.cpp main.cpp
COSAFETYFILES = $(PARSERFILES) $(UTILFILES) formula/aalta_formula.cpp cosafety2smv.cpp
CC = g++
FLAG = -I./ -I./minisat/ -I./formula/ -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS
DEBUGFLAG = -g -pg
RELEASEFLAG = -O2
aalta : release
ltlparser/ltllexer.c :
ltlparser/grammar/ltllexer.l
flex ltlparser/grammar/ltllexer.l
ltlparser/ltlparser.c :
ltlparser/grammar/ltlparser.y
bison ltlparser/grammar/ltlparser.y
cosafety2smv : $(COSAFETYFILES)
$(CC) $(FLAG) $(DEBUGFLAG) $(COSAFETYFILES) -lz -o cosafety2smv
.PHONY : release debug clean
release : $(ALLFILES)
$(CC) $(FLAG) $(RELEASEFLAG) $(ALLFILES) -lz -o aalta
debug : $(ALLFILES)
$(CC) $(FLAG) $(DEBUGFLAG) $(ALLFILES) -lz -o aalta
clean :
rm -f *.o *~ aalta
#!/usr/bin/perl
use File::Find;
use POSIX qw/strftime/;
use Time::HiRes qw( time );
#print strftime('%D %T',localtime);
$start = strftime('%D %T',localtime);
my $files;
find(\&wanted, 'benchmarks');
$n = 1;
#open(TIMEOUTFILE, ">timeout_aalta") or die "cannot open the file!";
#open(TIMEOUTFILE, ">error") or die "cannot open the file!";
foreach(@content)
{
if(-f $_)
{
#print "$_\n";
if($_ =~ /.*\.alaska/)
{
open(INFILE, "$_") or die "cannot open the input file!";
open(OUTFILE, ">output/$_") or die "cannot open the file!";
#open(TIMEOUTFILE, ">>output/timeout_aalta") or die "cannot open the file!";
$line = <INFILE>;
while ($line ne "")
{
eval
{
local $SIG{ALRM} = sub { die "timeout\n" };
alarm(60);
$t0 = time();
#print "checking\ $_ ...\n";
$output = `./aalta -fd "$line"`;
print OUTFILE "$output\n";
$n = $n + 1;
alarm(0);
};
if($@)
{
#print TIMEOUTFILE ("$_\n");
$output = `killall -9 aalta`;
print OUTFILE "timeout\n";
$n = $n + 1;
sleep 1;
}
$line = <INFILE>;
}
close(INFILE);
#close(OUTFILE);
}
}
}
close(TIMEOUTFILE);
$end = strftime('%D %T',localtime);
open(TIMEFILE, ">timeinfo") or die "cannot open the file!";
print TIMEFILE ("start time: $start\n");
print TIMEFILE ("end time: $end\n");
close(TIMEFILE);
exit;
sub wanted
{
push @content, $File::Find::name;
return;
}
#!/usr/bin/perl
use File::Find;
use POSIX qw/strftime/;
use Time::HiRes qw( time );
#print strftime('%D %T',localtime);
$start = strftime('%D %T',localtime);
my $files;
find(\&wanted, 'benchmarks');
$n = 1;
#open(TIMEOUTFILE, ">timeout_aalta") or die "cannot open the file!";
#open(TIMEOUTFILE, ">error") or die "cannot open the file!";
foreach(@content)
{
if(-f $_)
{
#print "$_\n";
if($_ =~ /.*\.alaska/)
{
open(INFILE, "$_") or die "cannot open the input file!";
open(OUTFILE, ">output/$_") or die "cannot open the file!";
#open(TIMEOUTFILE, ">>output/timeout_aalta") or die "cannot open the file!";
$line = <INFILE>;
while ($line ne "")
{
eval
{
local $SIG{ALRM} = sub { die "timeout\n" };
alarm(60);
$t0 = time();
#print "checking\ $_ ...\n";
$output = `./aalta -fn "$line"`;
print OUTFILE "$output\n";
$n = $n + 1;
alarm(0);
};
if($@)
{
#print TIMEOUTFILE ("$_\n");
$output = `killall -9 aalta`;
print OUTFILE "timeout\n";
$n = $n + 1;
sleep 1;
}
$line = <INFILE>;
}
close(INFILE);
#close(OUTFILE);
}
}
}
close(TIMEOUTFILE);
$end = strftime('%D %T',localtime);
open(TIMEFILE, ">timeinfo") or die "cannot open the file!";
print TIMEFILE ("start time: $start\n");
print TIMEFILE ("end time: $end\n");
close(TIMEFILE);
exit;
sub wanted
{
push @content, $File::Find::name;
return;
}
/*
* aiger translator to aalta_formula
* File: AIGER.cpp
* Author: Jianwen Li
*
* Created on November 19, 2014
*/
#include "AIGER.h"
#include "formula/aalta_formua.h"
#include <string>
#include <stdio.h>
#include <stdlib.h>
using namespace std;
aalta_formula* aiger_to_ltl (const string& fn, bool safety)
{
//get aiger object
aiger* aig = aiger_init ();
aiger_open_and_read_from_file(aig, fn.c_str());
const char * err = aiger_error(aig);
if (err)
{
cout << err << endl;
throw InputError(err);
}
if (!aiger_is_reencoded(aig))
aiger_reencode(aig);
if (safety) //safety property
return aiger_safety (aig);
else
return aiger_fair (aig);
}
aalta_formula* aiger_safety (aiger *aig)
{
aalta_formula *result, *constraint, *output, *bad;
result = NULL;
constraint = NULL;
output = NULL;
bad = NULL;
for (size_t i = 0; i < aig->num_constraints; ++i)
{
if (i == 0)
constraint = generate_constraint (aig, 0);
else
constraint = aalta_formula (aalta_formula::And, constraint, generate_constraint (aiger, i)).unique ();
}
/* not sure for the outputs!!
for (size_t i = 0; i < aig->num_outputs; ++i)
{
if (i == 0)
output = generate_output (aig, 0);
else
output = aalta_formula (aalta_formula::Or, output, generate_output (aiger, i)).unique ();
}
*/
for (size_t i = 0; i < aig->num_bad; ++i)
{
if (i == 0)
bad = generate_bad (aig, 0);
else
bad = aalta_formula (aalta_formula::Or, bad, generate_bad (aiger, i)).unique ();
}
if (constraint == NULL)
{
if (bad != NULL)
result = bad;
}
else
{
assert (bad != NULL);
bad = aalta_formula (aalta_formula::And, constraint, bad).unique ();
result = aalta_formula (aalta_formula::Until, constraint, bad).unique ();
}
return result;
}
aalta_formula* generate_constraint (aiger *aig, unsigned pos)
{
unsigned id = aig->constraints[pos].lit;
aalta_formula *result = generate_formula (aig, id);
return result;
}
aalta_formula* generate_bad (aiger *aig, unsigned pos)
{
unsigned id = aig->bad[pos].lit;
aalta_formula *result = generate_formula (aig, id);
return result;
}
aalta_formula* aiger_fair (aiger* aig)
{
aalta_formula *result, *fair, *justice, *f, *g;
result = NULL;
for (size_t i = 0; i < aig->num_constraints; ++i)
{
if (i == 0)
result = generate_constraint (aig, 0);
else
result = aalta_formula (aalta_formula::And, result, generate_constraint (aiger, i)).unique ();
}
if (result != NULL)
result = aalta_formula (aalta_formula::Release, aalta_formula::FALSE (), result).unique ();
for (size_t i = 0; i < aig->num_fairness; ++i)
{
fair = generate_fair (aig, i);
f = aalta_formula (aalta_formula::Until, aalta_formula::TRUE (), fair).unique ();
g = aalta_formula (aalta_formula::Release, aalta_formula::FALSE (), f).unique ();
if (result == NULL)
result = g;
else
result = aalta_formula (aalta_formula::And, result, g).unique ();
}
for (size_t i = 0; i < aig->num_justice; ++i)
{
justice = generate_justice (aig, i);
if (result == NULL)
result = justice;
else
result = aalta_formula (aalta_formula::Or, result, justice).unique ();
}
return result;
}
aalta_formula* generate_fair (aiger *aig, unsigned pos)
{
unsigned id = aig->fairness[pos].lit;
aalta_formula *result = generate_formula (aig, id);
return result;
}
aalta_formula* generate_justice (aiger *aig, unsigned pos)
{
const aiger_symbol & sym = aig->justice[pos];
aalta_formula *result, *just, *f, *g;
result = NULL;
for (size_t j = 0; j < sym.size; ++j)
{
just = generate_formula (aig, sym.lits[j]);
f = aalta_formula (aalta_formula::Until, aalta_formula::TRUE (), fair).unique ();
g = aalta_formula (aalta_formula::Release, aalta_formula::FALSE (), f).unique ();
if (result == NULL)
result = g;
else
result = aalta_formula (aalta_formula::And, result, g).unique ();
}
return result;
}
aalta_formula* generate_formula (aiger *aig, unsigned id)
{
unsigned pos = id / 2;
aalta_formula *result;
if (FORMULAS[pos] != NULL)
result = FORMULAS[pos];
else
{
unsigned index;
aalta_formula *f, *l, *r;
for (size_t i = 0; i < aig->num_inputs; ++i)
{
index = aig->inputs[i].lit / 2;
if (FORMULAS[index] == NULL)
FORMULAS[index] = aalta_formula (index).unique ();
if (pos == index)
{
result = FORMULAS[index];
break;
}
}
for (size_t i = 0; i < aig->num_ands; ++i)
{
const aiger_and * aa = aig->ands + i;
index = aa->lhs / 2;
if (FORMULAS[index] == NULL)
{
l = generate_formula (aig, aa->rhs0);
r = generate_formula (aig, aa->rhs1);
f = aalta_formula (aalta_formula::And, l, r).unique ();
FORMULAS[index] = f;
}
if (pos == index)
{
result = FORMULAS[index];
break;
}
}
for (size_t i = 0; i < aig->num_latches, ++i)
{
index = aig->latches[i].lit / 2;
if (FORMULAS[index] == NULL)
FORMULAS[index] = aalta_formula (index).unique ();
if (id == index)
{
result = FORMULAS[index];
break;
}
unsigned next = aig->latches[i].next / 2;
if (FORMULAS[next] == NULL)
FORMULAS[next] = aalta_formula (aalta_formula::Next, NULL, FORMULAS[index]).unique ();
if (pos == next)
{
result = FORMULAS[next];
break;
}
}
if (id % 2 != 0)
{
result = aalta_formula (aalta_formula::Not, NULL, result).unique ();
result = result->nnf ();
}
}
return result;
}
This diff is collapsed.
This diff is collapsed.
/***************************************************************************
Copyright (c) 2006 - 2011, Armin Biere, Johannes Kepler University.
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to
deal in the Software without restriction, including without limitation the
rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in
all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS
IN THE SOFTWARE.
***************************************************************************/
/*------------------------------------------------------------------------*/
/* This file contains the API of the 'AIGER' library, which is a reader and
* writer for the AIGER AIG format. The code of the library
* consists of 'aiger.c' and 'aiger.h'. It is independent of 'simpaig.c'
* and 'simpaig.h'.
* library.
*/
#ifndef aiger_h_INCLUDED
#define aiger_h_INCLUDED
#include <stdio.h>
/*------------------------------------------------------------------------*/
#define AIGER_VERSION "1.9"
/*------------------------------------------------------------------------*/
typedef struct aiger aiger;
typedef struct aiger_and aiger_and;
typedef struct aiger_symbol aiger_symbol;
/*------------------------------------------------------------------------*/
/* AIG references are represented as unsigned integers and are called
* literals. The least significant bit is the sign. The index of a literal
* can be obtained by dividing the literal by two. Only positive indices
* are allowed, which leaves 0 for the boolean constant FALSE. The boolean
* constant TRUE is encoded as the unsigned number 1 accordingly.
*/
#define aiger_false 0
#define aiger_true 1
#define aiger_sign(l) \
(((unsigned)(l))&1)
#define aiger_strip(l) \
(((unsigned)(l))&~1)
#define aiger_not(l) \
(((unsigned)(l))^1)
/*------------------------------------------------------------------------*/
/* Each literal is associated to a variable having an unsigned index. The
* variable index is obtained by deviding the literal index by two, which is
* the same as removing the sign bit.
*/
#define aiger_var2lit(i) \
(((unsigned)(i)) << 1)
#define aiger_lit2var(l) \
(((unsigned)(l)) >> 1)
/*------------------------------------------------------------------------*/
/* Callback functions for client memory management. The 'free' wrapper will
* get as last argument the size of the memory as it was allocated.
*/
typedef void *(*aiger_malloc) (void *mem_mgr, size_t);
typedef void (*aiger_free) (void *mem_mgr, void *ptr, size_t);
/*------------------------------------------------------------------------*/
/* Callback function for client character stream reading. It returns an
* ASCII character or EOF. Thus is has the same semantics as the standard
* library 'getc'. See 'aiger_read_generic' for more details.
*/
typedef int (*aiger_get) (void *client_state);
/*------------------------------------------------------------------------*/
/* Callback function for client character stream writing. The return value
* is EOF iff writing failed and otherwise the character 'ch' casted to an
* unsigned char. It has therefore the same semantics as 'fputc' and 'putc'
* from the standard library.
*/
typedef int (*aiger_put) (char ch, void *client_state);
/*------------------------------------------------------------------------*/
enum aiger_mode
{
aiger_binary_mode = 0,
aiger_ascii_mode = 1,
aiger_stripped_mode = 2, /* can be ORed with one of the previous */
};
typedef enum aiger_mode aiger_mode;
/*------------------------------------------------------------------------*/
struct aiger_and
{
unsigned lhs; /* as literal [2..2*maxvar], even */
unsigned rhs0; /* as literal [0..2*maxvar+1] */
unsigned rhs1; /* as literal [0..2*maxvar+1] */
};
/*------------------------------------------------------------------------*/
struct aiger_symbol
{
unsigned lit; /* as literal [0..2*maxvar+1] */
unsigned next, reset; /* used only for latches */
unsigned size, * lits; /* used only for justice */
char *name;
};
/*------------------------------------------------------------------------*/
/* This is the externally visible state of the library. The format is
* almost the same as the ASCII file format. The first part is exactly as
* in the header 'M I L O A' and optional 'B C J F' after the format identifier
* string.
*/
struct aiger
{
/* variable not literal index, e.g. maxlit = 2*maxvar + 1
*/
unsigned maxvar;
unsigned num_inputs;
unsigned num_latches;
unsigned num_outputs;
unsigned num_ands;
unsigned num_bad;
unsigned num_constraints;
unsigned num_justice;
unsigned num_fairness;
aiger_symbol *inputs; /* [0..num_inputs[ */
aiger_symbol *latches; /* [0..num_latches[ */
aiger_symbol *outputs; /* [0..num_outputs[ */
aiger_symbol *bad; /* [0..num_bad[ */
aiger_symbol *constraints; /* [0..num_constraints[ */
aiger_symbol *justice; /* [0..num_justice[ */
aiger_symbol *fairness; /* [0..num_fairness[ */
aiger_and *ands; /* [0..num_ands[ */
char **comments; /* zero terminated */
};
/*------------------------------------------------------------------------*/
/* Version and CVS identifier.
*/
const char *aiger_id (void);
const char *aiger_version (void);
/*------------------------------------------------------------------------*/
/* You need to initialize the library first. This generic initialization
* function uses standard 'malloc' and 'free' from the standard library for