Commit 6d213e5e authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Remove the Nips interface.

* NEWS: Mention it.
* configure.ac, README: Remove it.
* iface/Makefile.am (SUBDIRS): Remove nips.
* iface/nips/: Delete this directory.
parent 8256ae9b
2011-03-07 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Remove the Nips interface.
* NEWS: Mention it.
* configure.ac, README: Remove it.
* iface/Makefile.am (SUBDIRS): Remove nips.
* iface/nips/: Delete this directory.
2011-03-07 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Accept "P_0 == CS" as synonym for "P_0.CS" in the dve2 interface.
......
New in spot 0.7.1a:
* Spot can read DiVinE models. See iface/dve2/README for details.
* The experimental Nips interface has been removed.
New in spot 0.7.1 (2001-02-07):
......
......@@ -148,8 +148,6 @@ iface/ Interfaces to other libraries.
dve2/ Interface with DiVinE2.
gspn/ GreatSPN interface.
examples/ Supporting models used by the test cases.
nips/ NIPS interface (to use Promela models).
nipstest/ Tests for NIPS.
Third party software
--------------------
......@@ -157,10 +155,6 @@ Third party software
buddy/ A patched version of BuDDy 2.3 (a BDD library).
lbtt/ lbtt 1.2.1 (an LTL to Büchi automata test bench).
ltdl/ Libtool's portable dlopen() wrapper library.
iface/ Interfaces to other libraries.
nips/ NIPS interface (to use Promela models).
nips_vm/ NIPS VM 1.2.7 (New Implementation of Promela Semantics
Virtual Machine).
Build-system stuff
------------------
......@@ -179,4 +173,3 @@ End:
LocalWords: gtec Tarjan tgbaparse tgbatest doc html PDF spotref pdf cgi ELTL
LocalWords: CGI ltl iface BDD Couvreur's evtgba emptchk kripke Kripke saba vm
LocalWords: eltlparse eltltest SABA sabaalgos sabatest ssp ltlcouter scc SCC
LocalWords: Promela nipstest VM
......@@ -103,10 +103,6 @@ AC_CONFIG_FILES([
iface/gspn/defs
iface/gspn/Makefile
iface/Makefile
iface/nips/Makefile
iface/nips/nipstest/defs
iface/nips/nipstest/Makefile
iface/nips/nips_vm/Makefile
src/eltlparse/Makefile
src/eltltest/defs
src/eltltest/Makefile
......
......@@ -21,7 +21,7 @@
## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
## 02111-1307, USA.
SUBDIRS = nips dve2
SUBDIRS = dve2
if WITH_GSPN
SUBDIRS += gspn
......
TAGS
dottynips
empt_check
## Copyright (C) 2008 Laboratoire de Recherche et Développement
## de l'Epita (LRDE).
##
## This file is part of Spot, a model checking library.
##
## Spot 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.
##
## Spot 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 Spot; see the file COPYING. If not, write to the Free
## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
## 02111-1307, USA.
AM_CPPFLAGS = -I$(top_srcdir)/src $(BUDDY_CPPFLAGS) -I$(srcdir)/nips_vm
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
nipsdir = $(pkgincludedir)/iface/nips
nips_HEADERS = \
common.hh \
nips.hh
lib_LTLIBRARIES = libspotnips.la
libspotnips_la_LIBADD = $(top_builddir)/src/libspot.la $(builddir)/nips_vm/libnipsvm.la
libspotnips_la_SOURCES = \
common.cc \
nips.cc
noinst_PROGRAMS = \
dottynips empt_check
dottynips_SOURCES = dottynips.cc
dottynips_LDADD = libspotnips.la
empt_check_SOURCES = emptiness_check.cc
empt_check_LDADD = libspotnips.la
SUBDIRS = nips_vm nipstest
// Copyright (C) 2008 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
// Spot 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.
//
// Spot 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include "common.hh"
#include <ostream>
namespace spot
{
std::ostream&
operator<<(std::ostream& os, const nips_exception& e)
{
if (e.get_err_defined())
os << e.get_where() << " with exit value: " << e.get_err();
else
os << e.get_where();
return os;
}
}
// Copyright (C) 2008 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
// Spot 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.
//
// Spot 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#ifndef SPOT_IFACE_NIPS_COMMON_HH
# define SPOT_IFACE_NIPS_COMMON_HH
# include <string>
# include <iosfwd>
namespace spot
{
/// An exception used to forward NIPS errors.
class nips_exception
{
public:
nips_exception(const std::string& where, int err)
: err_(err), where_(where), err_defined_(true)
{
}
nips_exception(const std::string& where)
: err_(-1), where_(where), err_defined_(false)
{
}
int
get_err() const
{
return err_;
}
std::string
get_where() const
{
return where_;
}
int
get_err_defined() const
{
return err_defined_;
}
private:
int err_;
std::string where_;
bool err_defined_;
};
std::ostream& operator<<(std::ostream& os, const nips_exception& e);
}
#endif // SPOT_IFACE_NIPS_COMMON_HH
#! /bin/bash
NIPS_COMPILER=~/lrde/vmssg/nips_c/CodeGen
NIPS_ASSEMBLER=~/lrde/vmssg/nips_vm/nips_asm.pl
THISDIR=`pwd`
if [ ! -f "$NIPS_COMPILER" ]; then
echo "You have to specify the path of your NIPS compiler (CodeGen)"
exit 3
fi
if [ ! -f "$NIPS_ASSEMBLER" ]; then
echo "You have to specify the path of your NIPS assembler (nips_asm.pl)"
exit 3
fi
if [ $# -ne 1 ]; then
echo "usage : $0 promela_model"
exit 1
fi
FILE="$(cd `dirname $1`; pwd)/`basename $1`"
TMP_FILE="/tmp/`basename $1`"
cpp "$FILE" | sed 's/^#.*$//' > "$TMP_FILE"
cd `dirname $NIPS_COMPILER`
./`basename $NIPS_COMPILER` "$TMP_FILE"
cd `dirname $NIPS_ASSEMBLER`
./`basename $NIPS_ASSEMBLER` "$TMP_FILE.s"
mv "$TMP_FILE.b" "$FILE.b"
echo "$FILE".b
// Copyright (C) 2008 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
// Spot 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.
//
// Spot 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include <cstdlib>
#include "nips.hh"
#include "tgbaalgos/dotty.hh"
int
main(int argc, char **argv)
try
{
if (argc < 2)
{
std::cerr << "usage: " << argv[0] << " promela_bytecode" << std::endl;
exit(1);
}
spot::bdd_dict* dict = new spot::bdd_dict();
spot::nips_interface nips(dict, argv[1]);
spot::tgba* a = nips.automaton();
spot::dotty_reachable(std::cout, a);
delete a;
delete dict;
}
catch (spot::nips_exception& e)
{
std::cerr << e << std::endl;
return 1;
}
// Copyright (C) 2008 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 Spot, a model checking library.
//
// Spot 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.
//
// Spot 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include <cstdlib>
#include <iostream>
#include <cassert>
#include <cstring>
#include "common.hh"
#include "nips.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gtec/ce.hh"
#include "tgbaalgos/projrun.hh"
void
display_stats(const spot::unsigned_statistics* s)
{
assert(s);
spot::unsigned_statistics::stats_map::const_iterator i;
for (i = s->stats.begin(); i != s->stats.end(); ++i)
std::cout << i->first << " = " << (s->*i->second)() << std::endl;
}
int
main(int argc, char **argv)
try
{
// enum {Couvreur, Couvreur2} check = Couvreur;
bool compute_counter_example = true;
if (argc < 2)
{
std::cerr << "usage: " << argv[0] << "[OPTIONS...] promela_bytecode"
<< std::endl
<< "with OPTIONS :" << std::endl
<< " -c compute an example" << std::endl
<< " (instead of just checking for emptiness)" << std::endl
<< " -eALGO use ALGO emptiness-check (default)" << std::endl
<< "Where ALGO should be one of:" << std::endl
<< " Cou99(OPTIONS) (the default)" << std::endl
<< " CVWY90(OPTIONS)" << std::endl
<< " GV04(OPTIONS)" << std::endl
<< " SE05(OPTIONS)" << std::endl
<< " Tau03(OPTIONS)" << std::endl
<< " Tau03_opt(OPTIONS)" << std::endl;
exit(2);
}
int arg_index = 1;
spot::emptiness_check_instantiator* echeck_inst = 0;
const char* echeck_algo = "Cou99";
for (; arg_index < argc - 1; ++arg_index)
{
if (!strcmp(argv[arg_index], "-c"))
compute_counter_example = false;
else if (!strncmp(argv[arg_index], "-e", 2))
{
echeck_algo = 2 + argv[arg_index];
if (!*echeck_algo)
echeck_algo = "Cou99";
}
}
const char* err;
echeck_inst =
spot::emptiness_check_instantiator::construct(echeck_algo, &err);
if (!echeck_inst)
{
std::cerr << "Failed to parse argument of -e near `"
<< err << "'" << std::endl;
exit(2);
}
spot::bdd_dict* dict = new spot::bdd_dict();
spot::nips_interface nips(dict, argv[arg_index]);
spot::tgba* a = nips.automaton();
spot::emptiness_check* ec = echeck_inst->instantiate(a);
spot::emptiness_check_result* res = ec->check();
if (res)
{
if (compute_counter_example)
{
spot::tgba_run* run = res->accepting_run();
spot::print_tgba_run(std::cout, a, run);
std::cout << "non empty" << std::endl;
ec->print_stats(std::cout);
delete run;
}
else
{
std::cout << "non empty" << std::endl;
ec->print_stats(std::cout);
}
delete res;
}
else
{
std::cout << "empty" << std::endl;
ec->print_stats(std::cout);
}
std::cout << std::endl;
delete ec;
}
catch (spot::nips_exception& e)
{
std::cerr << e << std::endl;
return 1;
}
// Copyright (C) 2008, 2010, 2011 Laboratoire de Recherche et Dveloppement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
// Spot 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.
//
// Spot 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include <cassert>
#include "misc/hashfunc.hh"
#include "nips.hh"
#include "nipsvm.h"
namespace spot
{
namespace
{
// Callback for errors
//////////////////////////////////////////////////////////////////////
// Callback for error which continues on assertions
nipsvm_status_t
search_error_callback(nipsvm_errorcode_t err, nipsvm_pid_t pid,
nipsvm_pc_t pc, void *)
{
char str[256];
nipsvm_errorstring (str, sizeof str, err, pid, pc);
std::cerr << "RUNTIME ERROR (" << err << "): " << str << std::endl;
// Continue on assertions
if (err == 9)
return IC_CONTINUE;
throw nips_exception(std::string(str), static_cast<int>(err));
return IC_STOP;
}
// Callback for error which fails on assertions
// nipsvm_status_t
// search_error_callback_assert(nipsvm_errorcode_t err, nipsvm_pid_t pid,
// nipsvm_pc_t pc, void *)
// {
// char str[256];
//
// nipsvm_errorstring (str, sizeof str, err, pid, pc);
// std::cerr << "RUNTIME ERROR (" << err << "): " << str << std::endl;
//
// throw nips_exception(std::string(str), static_cast<int>(err));
// return IC_STOP;
// }
// state_nips
//////////////////////////////////////////////////////////////////////
class state_nips: public state
{
public:
state_nips(nipsvm_state_t* s)
: ref_(new unsigned(1))
{
unsigned long size = nipsvm_state_size(s);
unsigned long size_buf = size;
char* state_as_char = new char[size];
state_ = reinterpret_cast<nipsvm_state_t*>(state_as_char);
nipsvm_state_copy(size, s, &state_as_char, &size_buf);
hash_comp();
}
state_nips(const state* other)
{
const state_nips* o = dynamic_cast<const state_nips*>(other);
assert(o);
ref_ = o->ref_;
++(*ref_);
state_ = o->state_;
hash_ = o->hash_;
}
virtual
~state_nips()
{
--(*ref_);
if (*ref_ == 0)
{
delete[] state_;
delete ref_;
}
}
/// Lazy computation for the hash.
void
hash_comp()
{
size_t size = nipsvm_state_size(get_state());
hash_ = 0;
size_t* state = reinterpret_cast<size_t*>(get_state());
size_t full_size = (size - (size % sizeof (size_t))) / sizeof (size_t);
unsigned i;
for (i = 0; i < full_size; ++i)
hash_ ^= wang32_hash(state[i]);
// Hash on the remainder.
unsigned remainder = 0;
char* state_in_char = reinterpret_cast<char*>(state);
size_t init_pos = i * sizeof (size_t);
unsigned j;
for (j = 0; j < (size % sizeof (size_t)); ++j)
remainder = remainder * 0x100 + state_in_char[init_pos + j];
for (; j < sizeof (size_t); ++j)
remainder *= 0x100;
hash_ ^= remainder;
}
virtual int
compare(const state* other) const
{
const state_nips* o = dynamic_cast<const state_nips*>(other);
assert(o);
return nipsvm_state_compare(get_state(), o->get_state(),
min(nipsvm_state_size(get_state()),
nipsvm_state_size(o->get_state())));
}
virtual size_t
hash() const
{
return hash_;
}
virtual state_nips* clone() const
{
return new state_nips(get_state());
}
nipsvm_state_t*
get_state() const
{
return state_;
}
private:
unsigned* ref_;
nipsvm_state_t* state_;
size_t hash_;
}; // state_nips
// Callback for successors
//////////////////////////////////////////////////////////////////////
nipsvm_status_t
successor_state_callback(size_t, nipsvm_state_t *succ,
nipsvm_transition_information_t *,
void *context)
{
std::list<state_nips*> *succ_list =
reinterpret_cast<std::list<state_nips*>*>(context);
succ_list->push_back(new state_nips(succ));
return IC_CONTINUE;
}
// tgba_succ_iterator_nips
//////////////////////////////////////////////////////////////////////