Commit 5e8be97b authored by Etienne Renault's avatar Etienne Renault
Browse files

Fix compilation problems

* src/main.cpp: Fix merging problems.
parents 7a2fdbc4 938402d2
......@@ -14,3 +14,4 @@ missing
*.o
stamp
ylwrap
.DS_Store
SUBDIRS= libpn src doc
EXTRA_DIST = \
samples/fms2.net \
samples/fms3.net \
samples/fms4.net \
samples/kanban2.net \
samples/kanban3.net \
samples/kanban4.net \
samples/philo5.net \
samples/philo6.net \
samples/philo7.net \
samples/philo8.net \
samples/philo9.net \
samples/ring5.net \
samples/ring6.net \
samples/simple.net
#SUBDIRS=Generators
SUBDIRS=libpn src
EXTRA_DIST= \
alternateFIFO.net \
fms5.net \
Petrucci/5AGV_controlled.net \
Petrucci/5AGV.eps \
Petrucci/5AGV.net \
Petrucci/5AGV.pn \
Petrucci/prop \
Petrucci/prop2 \
philo2.100.net \
philo2.20.net \
philo2.5.net \
simple.net \
alternateInhibitor.net \
fms10.net \
Garavel/benchResults.txt \
Garavel/Lotos-Garavel.net \
Garavel/origin.txt \
Garavel/quasi-live.prop \
kanban5.net \
pgcd.net \
philo2.10.net \
philo2.50.net \
ring10.net
DISTCHECK_CONFIGURE_FLAGS=--with-spot=$(spot_prefix)
\ No newline at end of file
......@@ -7,6 +7,7 @@ AC_ARG_WITH([spot], [prefix of the spot installation], [
AC_PROG_CXX
AC_PROG_RANLIB
AM_PROG_AR
AM_PROG_LEX
AC_PROG_YACC
......
......@@ -9,4 +9,10 @@ libpn_a_SOURCES = \
pnscan.ll \
pnparse.yy
AM_YFLAGS = -d
BUILT_SOURCES = pnparse.h
\ No newline at end of file
BUILT_SOURCES = pnparse.h
pnparse.h:
bison -o pnparse.h -d pnparse.yy
AM_CPPFLAGS = -I$(spot_prefix)/include/spot
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
......@@ -27,60 +29,18 @@
#include <iostream>
#include "compressedmarking.hh"
#include "misc/intvcomp.hh"
compressed_marking::compressed_marking(const compressed_marking& m) : mac(m.mac) {
}
compressed_marking::compressed_marking(const marking& m) : mac() {
int i, j, nbp = m.size();
for (i=0; i<nbp; ++i) {
int p = m.get(i);
if (p<8) { // insert p false following by 1 true
for (j=0; j<p; ++j)
mac.push_back(false);
mac.push_back(true);
}
else { // insert 8 false following by p in reverse order
for (j=0; j<8; ++j)
mac.push_back(false);
const int mask = 1;
const int si=8*sizeof(int);
for (j=0; j<si; ++j, p>>=1)
if (mask & p)
mac.push_back(true);
else
mac.push_back(false);
}
}
spot::int_vector_vector_compress(m.get_vector(), mac);
}
marking* compressed_marking::expand() const {
marking* res = new marking;
int p=0, v=0, cpt=0;
std::vector<bool>::const_iterator it = mac.begin();
while (it!=mac.end()) {
if (!*it) {
++cpt;
++it;
if (cpt==8) { // the value follows
const int si=8*sizeof(int);
int mask = 1;
v=0;
for (int j=0;j<si;++j,++it,mask<<=1) {
if (*it) v+=mask;
}
res->append(v);
++p;
cpt=0;
}
} else {
++it;
res->append(cpt);
++p;
cpt=0;
}
}
marking* compressed_marking::expand(int psize) const {
marking* res = new marking();
spot::int_vector_vector_decompress(mac, res->get_vector(), psize);
return res;
}
......@@ -88,6 +48,6 @@ void compressed_marking::print(std::ostream& os) const {
std::copy(mac.begin(), mac.end(), std::ostream_iterator<bool>(os, " "));
}
const std::vector<bool>& compressed_marking::get_vector() const {
const std::vector<unsigned int>& compressed_marking::get_vector() const {
return mac;
}
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
......@@ -37,16 +39,19 @@ public:
compressed_marking(const marking& m);
/// Return the corresponding expanded marking.
marking* expand() const;
///
/// \param psize the size of the marking (the number of place in the petri
/// net).
marking* expand(int psize) const;
/// \brief Basic printing method (as a vector of bits).
void print(std::ostream& os) const;
/// \brief Return the std::vector<bool> coding the marking.
const std::vector<bool>& get_vector() const;
const std::vector<unsigned int>& get_vector() const;
protected:
std::vector<bool> mac;
std::vector<unsigned int> mac;
};
#endif
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of the Spot tutorial. Spot is a model checking
// This file is part of the Spot tutorial. Spot is a model checking
// library.
//
// Spot is free software; you can redistribute it and/or modify it
......@@ -55,33 +57,33 @@ int marking::size() const {
bool marking::operator<=(const marking& m) const {
assert(ma.size() == m.ma.size());
std::pair<std::vector<int>::const_iterator, std::vector<int>::const_iterator>
std::pair<std::vector<int>::const_iterator, std::vector<int>::const_iterator>
res = std::mismatch(
ma.begin(), ma.end(),
m.ma.begin(),std::less_equal<int>());
ma.begin(), ma.end(),
m.ma.begin(),std::less_equal<int>());
return res.first == ma.end();
}
bool marking::operator>=(const marking& m) const {
assert(ma.size() == m.ma.size());
std::pair<std::vector<int>::const_iterator, std::vector<int>::const_iterator>
std::pair<std::vector<int>::const_iterator, std::vector<int>::const_iterator>
res = std::mismatch(
ma.begin(), ma.end(),
m.ma.begin(),std::greater_equal<int>());
ma.begin(), ma.end(),
m.ma.begin(),std::greater_equal<int>());
return res.first == ma.end();
}
void marking::plus(const marking& m, marking& res) const {
assert(ma.size() == m.ma.size() && ma.size() == res.ma.size());
std::transform(
ma.begin(), ma.end(),
m.ma.begin(), res.ma.begin(),
std::plus<int>());
ma.begin(), ma.end(),
m.ma.begin(), res.ma.begin(),
std::plus<int>());
}
void marking::minus(const marking& m, marking& res) const {
......@@ -89,9 +91,9 @@ void marking::minus(const marking& m, marking& res) const {
assert(*this>=m);
std::transform(
ma.begin(), ma.end(),
m.ma.begin(), res.ma.begin(),
std::minus<int>());
ma.begin(), ma.end(),
m.ma.begin(), res.ma.begin(),
std::minus<int>());
}
void marking::print(std::ostream& os) const {
......@@ -102,7 +104,7 @@ void marking::print(std::ostream& os) const {
for (p=0, i = ma.begin(); i!=ma.end(); ++p, ++i) {
if (*i) {
if (b)
os << " + ";
os << " + ";
os << *i << ".p" << p;
b = true;
}
......@@ -114,3 +116,7 @@ void marking::print(std::ostream& os) const {
const std::vector<int>& marking::get_vector() const {
return ma;
}
std::vector<int>& marking::get_vector() {
return ma;
}
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
......@@ -69,6 +71,8 @@ public:
/// \brief Return the std::vector<int> coding the marking.
const std::vector<int>& get_vector() const;
/// \brief Return the std::vector<int> coding the marking.
std::vector<int>& get_vector();
protected:
std::vector<int> ma;
......
......@@ -33,7 +33,6 @@ static petri_net *pn;
static std::string tname;
extern FILE *yyin;
extern char yytext[];
int yylex();
......
This diff is collapsed.
......@@ -15,5 +15,5 @@ checkpn_SOURCES = \
printrg.cpp
checkpn_LDADD = ../libpn/libpn.a
checkpn_LDFLAGS = -L$(spot_prefix)/lib -lspot -lbdd
AM_CPPFLAGS = -I$(srcdir)/../libpn -I$(spot_prefix)/include/spot \
-I$(spot_prefix)/include
\ No newline at end of file
AM_CPPFLAGS = -std=c++11 -I$(srcdir)/../libpn -I$(spot_prefix)/include/spot \
-I$(spot_prefix)/include
// Copyright (C) 2010, 2012 Laboratoire de Recherche et dveloppement de
// Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et dveloppement de
// l'Epita.
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (SRC), Universit Pierre
......@@ -26,6 +26,7 @@
#include <fstream>
#include <string>
#include <cstring>
#include <chrono>
#include "ltlparse/public.hh"
......@@ -34,29 +35,49 @@
static
void syntax(const char* prog) {
std::cerr << "Usage: "<< prog << " [OPTIONS...] petri_net_file" << std::endl
<< "where OPTIONS are" << std::endl
<< "Actions:" << std::endl
<< " -c display the number of states and edges of the"
<< " reachability graph"
<< std::endl
<< " -e display a sequence (if any) of the net "
<< "satisfying the formula (implies -f or -F)" << std::endl
<< " -fformula check the formula" << std::endl
<< " -Fformula_file check the formula read from formula_file"
<< std::endl
<< " -g display the reachability graph"
<< std::endl
<< "Options of the formula transformation (implies -f or -F):"
<< std::endl
<< " -b branching postponement"
<< " (false by default)" << std::endl
<< " -l fair-loop approximation"
<< " (false by default)" << std::endl
<< " -x try to produce a more deterministic automaton"
<< " (false by default)" << std::endl
<< " -y do not merge states with same symbolic "
<< "representation (true by default)"
<< std::endl;
<< "where OPTIONS are" << std::endl
<< "Actions:" << std::endl
<< " -cn display the number of states and edges of the"
<< " reachability graph"
<< std::endl
<< " -e display a sequence (if any) of the net "
<< "satisfying the formula (implies -f or -F)" << std::endl
<< " -fformula check the formula" << std::endl
<< " -Fffile check the formula read from formula_file"
<< std::endl
<< " -g display the reachability graph"
<< std::endl
<< " -gf display the formula automaton" << std::endl
<< " -gp display the product automaton" << std::endl
<< " -S display statistics about automaton and product"
<< std::endl
<< " -c use a TGBA" << std::endl
<< " -ds use a BA"
<< std::endl
<< " -ta use a TA (Testing Automaton)" << std::endl
<< " -sta use a STA (Single-pass Testing Automata))"
<< std::endl
<< " -gta use a GTA (Generalized Testing Automata))"
<< std::endl
<< " -sgta use a SGTA (Single-pass Generalized Testing "
<< "Automata)" << std::endl
<< " -tgta use a TGTA (Transition-based Generalized Testing "
<< "Automaton)" << std::endl
<< " -nm do not minimize the automaton" << std::endl
<< " -2p force 2 passes for "
<< "testing-automaton emptiness check (i.e. disable the heuristic)"
<< std::endl
<< "Options of the formula transformation (implies -f or -F):"
<< std::endl
<< " -b branching postponement"
<< " (false by default)" << std::endl
<< " -l fair-loop approximation"
<< " (false by default)" << std::endl
<< " -x try to produce a more deterministic automaton"
<< " (false by default)" << std::endl
<< " -y do not merge states with same symbolic "
<< "representation (true by default)"
<< std::endl;
exit(2);
}
......@@ -71,6 +92,14 @@ int main(int argc, const char *argv[]) {
bool post_branching = false;
bool fair_loop_approx = false;
std::string ltl_string;
model_check_approach mca = TGBA;
bool automaton_dotty_output = false;
bool prod_dotty_output = false;
bool is_full_2_pass = false;
bool opt_minimize = true;
bool opt_stats = false;
bool ta_artificial_livelock = false;
bool ta_degeneralized = true;
int pn_index = 0;
for (;;) {
......@@ -79,12 +108,19 @@ int main(int argc, const char *argv[]) {
++pn_index;
if (!strcmp(argv[pn_index], "-b")) {
post_branching = true;
}
if (!strcmp(argv[pn_index], "-c")) {
if (!strcmp(argv[pn_index], "-cn")) {
count = true;
}
else if (!strncmp(argv[pn_index], "-c", 3)) {
mca = TGBA;
}
else if (!strncmp(argv[pn_index], "-ds", 3)) {
mca = BA;
}
else if (!strcmp(argv[pn_index], "-e")) {
ce_expected = true;
}
......@@ -96,29 +132,68 @@ int main(int argc, const char *argv[]) {
check = true;
std::ifstream fin(argv[pn_index]+2);
if (!fin) {
std::cerr << "Cannot open " << argv[pn_index]+2 << std::endl;
exit(2);
std::cerr << "Cannot open " << argv[pn_index]+2 << std::endl;
exit(2);
}
if (!std::getline(fin, ltl_string, '\0')) {
std::cerr << "Cannot read " << argv[pn_index]+2 << std::endl;
exit(2);
std::cerr << "Cannot read " << argv[pn_index]+2 << std::endl;
exit(2);
}
}
else if (!strcmp(argv[pn_index], "-g")) {
print_rg = true;
}
else if (!strcmp(argv[pn_index], "-gf")) {
automaton_dotty_output = true;
}
else if (!strcmp(argv[pn_index], "-gp")) {
prod_dotty_output = true;
}
else if (!strcmp(argv[pn_index], "-l")) {
fair_loop_approx = true;
}
else if (!strncmp(argv[pn_index], "-nm", 2)) {
opt_minimize = false;
}
else if (!strcmp(argv[pn_index], "-p")) {
print_pn = true;
}
else if (!strncmp(argv[pn_index], "-ta", 3)) {
mca = TA;
ta_artificial_livelock = false;
}
else if (!strncmp(argv[pn_index], "-sta", 3)) {
mca = TA;
ta_artificial_livelock = true;
}
else if (!strncmp(argv[pn_index], "-gta", 5)) {
mca = TA;
ta_artificial_livelock = false;
ta_degeneralized = false;
}
else if (!strncmp(argv[pn_index], "-sgta", 5)) {
mca = TA;
ta_artificial_livelock = true;
ta_degeneralized = false;
}
else if (!strncmp(argv[pn_index], "-tgta", 6)){
mca = TGTA;
}
else if (!strncmp(argv[pn_index], "-S", 2)) {
opt_stats = true;
}
else if (!strcmp(argv[pn_index], "-x")) {
fm_exprop_opt = true;
}
else if (!strcmp(argv[pn_index], "-y")) {
fm_symb_merge_opt = false;
}
else if (!strcmp(argv[pn_index], "-2p")) {
is_full_2_pass = true;
}
else {
break;
}
......@@ -137,16 +212,29 @@ int main(int argc, const char *argv[]) {
if (count)
count_markings(n);
if (check) {
spot::ltl::parse_error_list pel;
const spot::ltl::formula* f = spot::ltl::parse(ltl_string, pel);
if (!spot::ltl::format_parse_errors(std::cerr, ltl_string, pel))
model_check(n, f, ce_expected, fm_exprop_opt, fm_symb_merge_opt,
post_branching, fair_loop_approx);
f->destroy();
}
auto start_time = std::chrono::high_resolution_clock::now();
spot::ltl::parse_error_list pel;
const spot::ltl::formula* f = spot::ltl::parse(ltl_string, pel);
if (!spot::ltl::format_parse_errors(std::cerr, ltl_string, pel))
model_check(n, f, ce_expected, mca,
fm_exprop_opt, fm_symb_merge_opt,
post_branching, fair_loop_approx,
opt_minimize, opt_stats, opt_stats,
automaton_dotty_output, prod_dotty_output,
is_full_2_pass, ta_artificial_livelock, ta_degeneralized);
f->destroy();
auto end_time = std::chrono::high_resolution_clock::now();
auto wall_cumul_ = std::chrono::duration_cast
<std::chrono::milliseconds>(end_time - start_time).count();
std::cout << "Walltime: " << wall_cumul_ << std::endl;
delete n;
return 0;
}
......@@ -3,42 +3,67 @@
#include "misc/timer.hh"
#include "ltlast/atomic_prop.hh"
#include "ltlvisit/apcollect.hh"
#include "ltlvisit/length.hh"
#include "ltlenv/environment.hh"
#include "ltlparse/public.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgba/tgbaproduct.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/dupexp.hh"
#include "tgbaalgos/dotty.hh"
#include "taalgos/dotty.hh"
#include "taalgos/emptinessta.hh"
#include "taalgos/minimize.hh"
#include "taalgos/tgba2ta.hh"
#include "taalgos/stats.hh"
#include "ta/taproduct.hh"
#include "ta/tgtaproduct.hh"
#include "tgbaalgos/degen.hh"
#include <chrono>
#include "pntgba.hh"
#include "pntgbautils.hh"
const std::string* check_at_prop(const petri_net* p,
const spot::ltl::formula* f) {
const std::string*
check_at_prop(const petri_net* p, const spot::ltl::formula* f)
{
spot::ltl::atomic_prop_set* sap = spot::ltl::atomic_prop_collect(f);
if (sap) {
spot::ltl::atomic_prop_set::iterator it;
for(it=sap->begin(); it!=sap->end(); ++it) {
if(!p->place_exists( (*it)->name() )) {
return &((*it)->name());
}
if (sap)
{
spot::ltl::atomic_prop_set::iterator it;
for (it = sap->begin(); it != sap->end(); ++it)
{
if (!p->place_exists((*it)->name()))
{
return &((*it)->name());
}
}
delete sap;
}
}
return 0;
} //
void model_check(const petri_net* n, const spot::ltl::formula* f,
bool ce_expected, bool fm_exprop_opt, bool fm_symb_merge_opt,
bool post_branching, bool fair_loop_approx) {
double start_time, build_time, check_time;
void
model_check(const petri_net* n, const spot::ltl::formula* f, bool ce_expected,
model_check_approach mca, bool fm_exprop_opt, bool fm_symb_merge_opt,
bool post_branching, bool fair_loop_approx, bool minimize,
bool automaton_stats, bool product_stats, bool formula_dotty_output,
bool product_dotty_output, bool force_2_passes,
bool is_ta_artificial_livelock, bool ta_degeneralized)
{
double start_time, build_time, check_time;
const std::string* s;
if ((s = check_at_prop(n, f))) {
std::cout << "the atomic proposition '" << *s
<< "' does not correspond to a place name" << std::endl;
return;
}
if ((s = check_at_prop(n, f)))
{
std::cout << "the atomic proposition '" << *s
<< "' does not correspond to a place name" << std::endl;
return;
}