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

@@ -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<spins_interface>();
     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");
+          sym("spins_get_successor_all");
-        d->get_state_size = (int (*)())
+        d->get_state_size = (int (*)()) sym("spins_get_state_size");
-        lt_dlsym(h, "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.
+    // dve2 and gal2C interfaces.
-    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.
     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.");

tests/ltsmin/check.test

@@ -1,7 +1,7 @@
 #!/bin/sh
 # -*- coding: utf-8 -*-
-# Copyright (C) 2011, 2012, 2014, 2015 Laboratoire de Recherche et
+# Copyright (C) 2011, 2012, 2014, 2015, 2016 Laboratoire de Recherche
-# Développement de l'Epita (LRDE).
+# 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.