Commit 51e6989d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Call divine to compile dve models.

* iface/dve2/dve2.cc (compile_dve2): New function.  Compile
the *.dve source if there is no newer *.dve2C already.
(load_dve2): Call compile_dve2 when given a *.dve file.
* iface/dve2/dve2.hh (load_dve2): Document it.
parent 4a622249
2011-03-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Call divine to compile dve models.
* iface/dve2/dve2.cc (compile_dve2): New function. Compile
the *.dve source if there is no newer *.dve2C already.
(load_dve2): Call compile_dve2 when given a *.dve file.
* iface/dve2/dve2.hh (load_dve2): Document it.
2011-03-06 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Allow atomic propositions and identifiers like `X.Y'.
......
......@@ -23,6 +23,8 @@
#include <cstdlib>
#include <vector>
#include <sstream>
#include <sys/stat.h>
#include <unistd.h>
#include "misc/hashfunc.hh"
#include "dve2.hh"
......@@ -582,7 +584,55 @@ namespace spot
////////////////////////////////////////////////////////////////////////////
// LOADER
kripke* load_dve2(const std::string& file_arg, bdd_dict* dict,
// Call divine to compile "foo.dve" as "foo.dve2C" if the latter
// does not exist already or is older.
bool
compile_dve2(std::string& filename, bool verbose)
{
std::string command = "divine compile --ltsmin " + filename;
struct stat s;
if (stat(filename.c_str(), &s) != 0)
{
if (verbose)
{
std::cerr << "Cannot open " << filename << std::endl;
return true;
}
}
std::string old = filename;
filename += "2C";
// Remove any directory, because the new file will
// be compiled in the current directory.
size_t pos = filename.find_last_of("/\\");
if (pos != std::string::npos)
filename = "./" + filename.substr(pos + 1);
struct stat d;
if (stat(filename.c_str(), &d) == 0)
if (s.st_mtime < d.st_mtime)
// The dve2C is up-to-date, no need to recompile it.
return false;
int res = system(command.c_str());
if (res)
{
if (verbose)
std::cerr << "Execution of `" << command.c_str()
<< "' returned exit code " << WEXITSTATUS(res)
<< "." << std::endl;
return true;
}
return false;
}
kripke*
load_dve2(const std::string& file_arg, bdd_dict* dict,
ltl::atomic_prop_set* to_observe, bool verbose)
{
std::string file;
......@@ -591,6 +641,25 @@ namespace spot
else
file = "./" + file_arg;
std::string ext = file.substr(file.find_last_of("."));
if (ext == ".dve")
{
if (compile_dve2(file, verbose))
{
if (verbose)
std::cerr << "Failed to compile `" << file_arg
<< "'." << std::endl;
return 0;
}
}
else if (ext != ".dve2C")
{
if (verbose)
std::cerr << "Unknown extension `" << ext
<< "'. Use `.dve' or `.dve2C'." << std::endl;
return 0;
}
if (lt_dlinit())
{
if (verbose)
......
......@@ -28,6 +28,22 @@
namespace spot
{
// \brief Load a DVE model.
//
// The filename given can be either a *.dve source or a *.dve2C
// dynamic library compiled with "divine compile --ltsmin file".
// When the *.dve source is supplied, the *.dve2C will be updated
// only if it is not newer.
//
// This function returns 0 on error.
//
// \a file the name of the *.dve source file or of the *.dve2C
// dynamic library
// \a to_observe the list of atomic propositions that should be observed
// in the model
// \a dict the BDD dictionary to use
// \a verbose whether to output verbose messages
kripke* load_dve2(const std::string& file,
bdd_dict* dict,
ltl::atomic_prop_set* to_observe,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment