From dc4a477172e4e59524178865c88c248cf3d3094e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 24 Nov 2016 10:26:46 +0100 Subject: [PATCH] lts-min: fix loading of spins models This fixes c9aabcdd. * spot/ltsmin/ltsmin.cc: Update the extension after compiling the model. Do not duplicate the symbol lookups for DVE and gal2C. Also, improve error reporting in case of missing symbol. * tests/ltsmin/check.test: Remove stray character. --- spot/ltsmin/ltsmin.cc | 92 +++++++++++++++-------------------------- tests/ltsmin/check.test | 6 +-- 2 files changed, 37 insertions(+), 61 deletions(-) diff --git a/spot/ltsmin/ltsmin.cc b/spot/ltsmin/ltsmin.cc index c79b2bf77..5efb04a95 100644 --- a/spot/ltsmin/ltsmin.cc +++ b/spot/ltsmin/ltsmin.cc @@ -1009,7 +1009,10 @@ namespace spot std::string ext = file.substr(file.find_last_of(".")); if (ext != ".spins" && ext != ".dve2C" && ext != ".gal2C") - compile_model(file, ext); + { + compile_model(file, ext); + ext = file.substr(file.find_last_of(".")); + } if (lt_dlinit()) throw std::runtime_error("Failed to initialize libltldl."); @@ -1026,90 +1029,63 @@ namespace spot auto d = std::make_shared(); d->handle = h; + + auto sym = [&](const char* name) + { + auto res = lt_dlsym(h, name); + if (res == nullptr) + throw std::runtime_error(std::string("Failed to resolve symbol '") + + name + "' in '" + file + "'."); + return res; + }; + // SpinS interface. if (ext == ".spins") { d->get_initial_state = (void (*)(void*)) - lt_dlsym(h, "spins_get_initial_state"); + sym("spins_get_initial_state"); d->have_property = nullptr; d->get_successors = (int (*)(void*, int*, TransitionCB, void*)) - lt_dlsym(h, "spins_get_successor_all"); - d->get_state_size = (int (*)()) - lt_dlsym(h, "spins_get_state_size"); + sym("spins_get_successor_all"); + d->get_state_size = (int (*)()) sym("spins_get_state_size"); d->get_state_variable_name = (const char* (*)(int)) - lt_dlsym(h, "spins_get_state_variable_name"); + sym("spins_get_state_variable_name"); d->get_state_variable_type = (int (*)(int)) - lt_dlsym(h, "spins_get_state_variable_type"); + sym("spins_get_state_variable_type"); d->get_type_count = (int (*)()) - lt_dlsym(h, "spins_get_type_count"); + sym("spins_get_type_count"); d->get_type_name = (const char* (*)(int)) - lt_dlsym(h, "spins_get_type_name"); + sym("spins_get_type_name"); d->get_type_value_count = (int (*)(int)) - lt_dlsym(h, "spins_get_type_value_count"); + sym("spins_get_type_value_count"); d->get_type_value_name = (const char* (*)(int, int)) - lt_dlsym(h, "spins_get_type_value_name"); + sym("spins_get_type_value_name"); } - // dve2 interface. - else if (ext == ".dve2C") - { - d->get_initial_state = (void (*)(void*)) - lt_dlsym(h, "get_initial_state"); - d->have_property = (int (*)()) - lt_dlsym(h, "have_property"); - d->get_successors = (int (*)(void*, int*, TransitionCB, void*)) - lt_dlsym(h, "get_successors"); - d->get_state_size = (int (*)()) - lt_dlsym(h, "get_state_variable_count"); - d->get_state_variable_name = (const char* (*)(int)) - lt_dlsym(h, "get_state_variable_name"); - d->get_state_variable_type = (int (*)(int)) - lt_dlsym(h, "get_state_variable_type"); - d->get_type_count = (int (*)()) - lt_dlsym(h, "get_state_variable_type_count"); - d->get_type_name = (const char* (*)(int)) - lt_dlsym(h, "get_state_variable_type_name"); - d->get_type_value_count = (int (*)(int)) - lt_dlsym(h, "get_state_variable_type_value_count"); - d->get_type_value_name = (const char* (*)(int, int)) - lt_dlsym(h, "get_state_variable_type_value"); - } - // .gal2C interface. + // dve2 and gal2C interfaces. else { d->get_initial_state = (void (*)(void*)) - lt_dlsym(h, "get_initial_state"); + sym("get_initial_state"); d->have_property = (int (*)()) - lt_dlsym(h, "have_property"); + lt_dlsym(h, "have_property"); d->get_successors = (int (*)(void*, int*, TransitionCB, void*)) - lt_dlsym(h, "get_successors"); + sym("get_successors"); d->get_state_size = (int (*)()) - lt_dlsym(h, "get_state_variable_count"); + sym("get_state_variable_count"); d->get_state_variable_name = (const char* (*)(int)) - lt_dlsym(h, "get_state_variable_name"); + sym("get_state_variable_name"); d->get_state_variable_type = (int (*)(int)) - lt_dlsym(h, "get_state_variable_type"); + sym("get_state_variable_type"); d->get_type_count = (int (*)()) - lt_dlsym(h, "get_state_variable_type_count"); + sym("get_state_variable_type_count"); d->get_type_name = (const char* (*)(int)) - lt_dlsym(h, "get_state_variable_type_name"); + sym("get_state_variable_type_name"); d->get_type_value_count = (int (*)(int)) - lt_dlsym(h, "get_state_variable_type_value_count"); + sym("get_state_variable_type_value_count"); d->get_type_value_name = (const char* (*)(int, int)) - lt_dlsym(h, "get_state_variable_type_value"); + sym("get_state_variable_type_value"); } - if (!(d->get_initial_state - && d->get_successors - && d->get_state_size - && d->get_state_variable_name - && d->get_state_variable_type - && d->get_type_count - && d->get_type_name - && d->get_type_value_count - && d->get_type_value_name)) - throw std::runtime_error(std::string("Failed to resolve some symbol " - "while loading '") + file + "'."); - if (d->have_property && d->have_property()) throw std::runtime_error("Models with embedded properties " "are not supported."); diff --git a/tests/ltsmin/check.test b/tests/ltsmin/check.test index fe1e7f919..d79e485fd 100755 --- a/tests/ltsmin/check.test +++ b/tests/ltsmin/check.test @@ -1,7 +1,7 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2011, 2012, 2014, 2015 Laboratoire de Recherche et -# Développement de l'Epita (LRDE). +# Copyright (C) 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche +# et Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. # @@ -79,7 +79,7 @@ for opt in '' '-z'; do run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.gal \ '!G("P_0.state==2" -> F "P_0.state==1")' - run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.gal '!G("pos[1] < 3")'a + run 0 ../modelcheck $opt -e $srcdir/beem-peterson.4.gal '!G("pos[1] < 3")' done # Now check some error messages.