alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltsmin: rework spins_interface

Browse source 
* spot/ltsmin/ltsmin.cc,
spot/ltsmin/spins_interface.cc,
spot/ltsmin/spins_interface.hh: here.
This commit is contained in:
Etienne Renault 2019-02-19 10:40:02 +01:00
parent 7a8a4f4d77
commit 949881935a
3 changed files with 175 additions and 155 deletions
Download patch file Download diff file Expand all files Collapse all files

145
spot/ltsmin/ltsmin.cc
View file

@ -26,11 +26,6 @@
#include <sys/stat.h>
#include <unistd.h>
// MinGW does not define this.
#ifndef WEXITSTATUS
# define WEXITSTATUS(x) ((x) & 0xff)
#endif
#include <spot/ltsmin/ltsmin.hh>
#include <spot/misc/hashfunc.hh>
#include <spot/misc/fixpool.hh>
@ -909,152 +904,14 @@ namespace spot
mutable bdd state_condition_last_cond_;
mutable callback_context* state_condition_last_cc_;
};
//////////////////////////////////////////////////////////////////////////
// LOADER
// Call spins to compile "foo.prom" as "foo.prom.spins" if the latter
// does not exist already or is older.
static void
compile_model(std::string& filename, const std::string& ext)
{
std::string command;
std::string compiled_ext;
if (ext == ".gal")
{
command = "gal2c " + filename;
compiled_ext = "2C";
}
else if (ext == ".prom" || ext == ".pm" || ext == ".pml")
{
command = "spins " + filename;
compiled_ext = ".spins";
}
else if (ext == ".dve")
{
command = "divine compile --ltsmin " + filename;
command += " 2> /dev/null"; // FIXME needed for Clang on MacOSX
compiled_ext = "2C";
}
else
{
throw std::runtime_error("Unknown extension '"s + ext +
"'. Use '.prom', '.pm', '.pml', "
"'.dve', '.dve2C', '.gal', '.gal2C' or "
"'.prom.spins'.");
}
struct stat s;
if (stat(filename.c_str(), &s) != 0)
throw std::runtime_error("Cannot open "s + filename);
filename += compiled_ext;
// 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 .spins or .dve2C or .gal2C is up-to-date, no need to compile.
return;
int res = system(command.c_str());
if (res)
throw std::runtime_error("Execution of '"s
+ command.c_str() + "' returned exit code "
+ std::to_string(WEXITSTATUS(res)));
}
}
ltsmin_model
ltsmin_model::load(const std::string& file_arg)
{
std::string file;
if (file_arg.find_first_of("/\\") != std::string::npos)
file = file_arg;
else
file = "./" + file_arg;
std::string ext = file.substr(file.find_last_of("."));
if (ext != ".spins" && ext != ".dve2C" && ext != ".gal2C")
{
compile_model(file, ext);
ext = file.substr(file.find_last_of("."));
}
if (lt_dlinit())
throw std::runtime_error("Failed to initialize libltldl.");
lt_dlhandle h = lt_dlopen(file.c_str());
if (!h)
{
std::string lt_error = lt_dlerror();
lt_dlexit();
throw std::runtime_error("Failed to load '"s
+ file + "'.\n" + lt_error);
}
auto d = std::make_shared<spins_interface>();
assert(d); // Superfluous, but Debian's GCC 7 snapshot 20161207-1 warns
// about potential null pointer dereference on the next line.
d->handle = h;
auto sym = [&](auto* dst, const char* name)
{
// Work around -Wpendantic complaining that pointer-to-objects
// should not be converted to pointer-to-functions (we have to
// assume they can for POSIX).
*reinterpret_cast<void**>(dst) = lt_dlsym(h, name);
if (dst == nullptr)
throw std::runtime_error("Failed to resolve symbol '"s
+ name + "' in '" + file + "'.");
};
// SpinS interface.
if (ext == ".spins")
{
sym(&d->get_initial_state, "spins_get_initial_state");
d->have_property = nullptr;
sym(&d->get_successors, "spins_get_successor_all");
sym(&d->get_state_size, "spins_get_state_size");
sym(&d->get_state_variable_name, "spins_get_state_variable_name");
sym(&d->get_state_variable_type, "spins_get_state_variable_type");
sym(&d->get_type_count, "spins_get_type_count");
sym(&d->get_type_name, "spins_get_type_name");
sym(&d->get_type_value_count, "spins_get_type_value_count");
sym(&d->get_type_value_name, "spins_get_type_value_name");
}
// dve2 and gal2C interfaces.
else
{
sym(&d->get_initial_state, "get_initial_state");
*reinterpret_cast<void**>(&d->have_property) =
lt_dlsym(h, "have_property");
sym(&d->get_successors, "get_successors");
sym(&d->get_state_size, "get_state_variable_count");
sym(&d->get_state_variable_name, "get_state_variable_name");
sym(&d->get_state_variable_type, "get_state_variable_type");
sym(&d->get_type_count, "get_state_variable_type_count");
sym(&d->get_type_name, "get_state_variable_type_name");
sym(&d->get_type_value_count, "get_state_variable_type_value_count");
sym(&d->get_type_value_name, "get_state_variable_type_value");
}
if (d->have_property && d->have_property())
throw std::runtime_error("Models with embedded properties "
"are not supported.");
return { d };
return {std::make_shared<spins_interface>(file_arg)};
}
ltsmin_kripkecube_ptr
ltsmin_model::kripkecube(std::vector<std::string> to_observe,
const formula dead, int compress,

162
spot/ltsmin/spins_interface.cc
View file

@ -17,17 +17,167 @@
// You should have received a copy of the GNU General Public License
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <config.h>
#include "config.h"
#include <spot/ltsmin/spins_interface.hh>
#include <ltdl.h>
#include <cstring>
#include <cstdlib>
#include <string.h>
#include <spot/mc/utils.hh>
#include <sys/stat.h>
// MinGW does not define this.
#ifndef WEXITSTATUS
# define WEXITSTATUS(x) ((x) & 0xff)
#endif
namespace spot
{
spins_interface::~spins_interface()
namespace
{
using namespace std::string_literals;
//////////////////////////////////////////////////////////////////////////
// LOADER
// Call spins to compile "foo.prom" as "foo.prom.spins" if the latter
// does not exist already or is older.
static void
compile_model(std::string& filename, const std::string& ext)
{
lt_dlhandle h = (lt_dlhandle) handle;
if (h)
lt_dlclose(h);
lt_dlexit();
std::string command;
std::string compiled_ext;
if (ext == ".gal")
{
command = "gal2c " + filename;
compiled_ext = "2C";
}
else if (ext == ".prom" || ext == ".pm" || ext == ".pml")
{
command = "spins " + filename;
compiled_ext = ".spins";
}
else if (ext == ".dve")
{
command = "divine compile --ltsmin " + filename;
command += " 2> /dev/null"; // FIXME needed for Clang on MacOSX
compiled_ext = "2C";
}
else
{
throw std::runtime_error("Unknown extension '"s + ext +
"'. Use '.prom', '.pm', '.pml', "
"'.dve', '.dve2C', '.gal', '.gal2C' or "
"'.prom.spins'.");
}
struct stat s;
if (stat(filename.c_str(), &s) != 0)
throw std::runtime_error("Cannot open "s + filename);
filename += compiled_ext;
// 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 .spins or .dve2C or .gal2C is up-to-date, no need to compile.
return;
int res = system(command.c_str());
if (res)
throw std::runtime_error("Execution of '"s
+ command.c_str() + "' returned exit code "
+ std::to_string(WEXITSTATUS(res)));
}
}
spins_interface::spins_interface(const std::string& file_arg)
{
std::string file;
if (file_arg.find_first_of("/\\") != std::string::npos)
file = file_arg;
else
file = "./" + file_arg;
std::string ext = file.substr(file.find_last_of("."));
if (ext != ".spins" && ext != ".dve2C" && ext != ".gal2C")
{
compile_model(file, ext);
ext = file.substr(file.find_last_of("."));
}
if (lt_dlinit())
throw std::runtime_error("Failed to initialize libltldl.");
lt_dlhandle h = lt_dlopen(file.c_str());
if (!h)
{
std::string lt_error = lt_dlerror();
lt_dlexit();
throw std::runtime_error("Failed to load '"s
+ file + "'.\n" + lt_error);
}
handle = h;
auto sym = [&](auto* dst, const char* name)
{
// Work around -Wpendantic complaining that pointer-to-objects
// should not be converted to pointer-to-functions (we have to
// assume they can for POSIX).
*reinterpret_cast<void**>(dst) = lt_dlsym(h, name);
if (dst == nullptr)
throw std::runtime_error("Failed to resolve symbol '"s
+ name + "' in '" + file + "'.");
};
// SpinS interface.
if (ext == ".spins")
{
sym(&get_initial_state, "spins_get_initial_state");
have_property = nullptr;
sym(&get_successors, "spins_get_successor_all");
sym(&get_state_size, "spins_get_state_size");
sym(&get_state_variable_name, "spins_get_state_variable_name");
sym(&get_state_variable_type, "spins_get_state_variable_type");
sym(&get_type_count, "spins_get_type_count");
sym(&get_type_name, "spins_get_type_name");
sym(&get_type_value_count, "spins_get_type_value_count");
sym(&get_type_value_name, "spins_get_type_value_name");
}
// dve2 and gal2C interfaces.
else
{
sym(&get_initial_state, "get_initial_state");
*reinterpret_cast<void**>(&have_property) =
lt_dlsym(h, "have_property");
sym(&get_successors, "get_successors");
sym(&get_state_size, "get_state_variable_count");
sym(&get_state_variable_name, "get_state_variable_name");
sym(&get_state_variable_type, "get_state_variable_type");
sym(&get_type_count, "get_state_variable_type_count");
sym(&get_type_name, "get_state_variable_type_name");
sym(&get_type_value_count, "get_state_variable_type_value_count");
sym(&get_type_value_name, "get_state_variable_type_value");
}
if (have_property && have_property())
throw std::runtime_error("Models with embedded properties "
"are not supported.");
}
spins_interface::~spins_interface()
{
lt_dlhandle h = (lt_dlhandle) handle;
if (h)
lt_dlclose(h);
lt_dlexit();
}
}

23
spot/ltsmin/spins_interface.hh
View file

@ -20,6 +20,7 @@
#pragma once
#include <memory>
#include <spot/misc/common.hh>
namespace spot
{
@ -36,11 +37,19 @@ namespace spot
transition_info_t *transition_info,
int *dst);
struct spins_interface
/// \brief Implementation of the PINS interface. This class
/// is a wrapper that, given a file, will compile it w.r.t
/// the PINS interface. The class can then be menipulated
/// transparently whatever the input format considered.
class SPOT_API spins_interface
{
// handle to the dynamic library. The variable is of type lt_dlhandle, but
// we need this trick since we cannot put ltdl.h in public headers
void* handle;
public:
spins_interface() = default;
spins_interface(const std::string& file_arg);
~spins_interface();
// The various functions that can be called once the object
// has been instanciated.
void (*get_initial_state)(void *to);
int (*have_property)();
int (*get_successors)(void* m, int *in, TransitionCB, void *arg);
@ -51,7 +60,11 @@ namespace spot
const char* (*get_type_name)(int type);
int (*get_type_value_count)(int type);
const char* (*get_type_value_name)(int type, int value);
~spins_interface();
private:
// handle to the dynamic library. The variable is of type lt_dlhandle, but
// we need this trick since we cannot put ltdl.h in public headers
void* handle;
};
using spins_interface_ptr = std::shared_ptr<const spins_interface>;