[mc] Cleanup/simplify liveness property automaton registration code

There were remants of the standalone mode.

diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 5440a68..85a8ecd 100644 (file)
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -517,38 +517,28 @@ void MC_automaton_load(const char *file)
   xbt_automaton_load(_mc_property_automaton, file);
 }
 
   xbt_automaton_load(_mc_property_automaton, file);
 }
 

-static void register_symbol(xbt_automaton_propositional_symbol_t symbol)
+void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void))
+{
+  xbt_die("Support for client-side function proposition is not implemented: "
+    "use MC_automaton_new_propositional_symbol_pointer instead."
+  );
+}
+
+void MC_automaton_new_propositional_symbol_pointer(const char *name, int* value)

 {
 {

+  xbt_assert(mc_mode != MC_MODE_SERVER);

   if (mc_mode != MC_MODE_CLIENT)
     return;
   s_mc_register_symbol_message_t message;
   message.type = MC_MESSAGE_REGISTER_SYMBOL;
   if (mc_mode != MC_MODE_CLIENT)
     return;
   s_mc_register_symbol_message_t message;
   message.type = MC_MESSAGE_REGISTER_SYMBOL;

-  const char* name = xbt_automaton_propositional_symbol_get_name(symbol);

   if (strlen(name) + 1 > sizeof(message.name))
     xbt_die("Symbol is too long");
   strncpy(message.name, name, sizeof(message.name));
   if (strlen(name) + 1 > sizeof(message.name))
     xbt_die("Symbol is too long");
   strncpy(message.name, name, sizeof(message.name));

-  message.callback = xbt_automaton_propositional_symbol_get_callback(symbol);
-  message.data = xbt_automaton_propositional_symbol_get_data(symbol);
+  message.callback = nullptr;
+  message.data = value;

   MC_client_send_message(&message, sizeof(message));
 }
 
   MC_client_send_message(&message, sizeof(message));
 }
 

-void MC_automaton_new_propositional_symbol(const char *id, int(*fct)(void))
-{
-  if (_mc_property_automaton == NULL)
-    _mc_property_automaton = xbt_automaton_new();
-
-  xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new(_mc_property_automaton, id, fct);
-  register_symbol(symbol);
-}
-
-void MC_automaton_new_propositional_symbol_pointer(const char *id, int* value)
-{
-  if (_mc_property_automaton == NULL)
-    _mc_property_automaton = xbt_automaton_new();
-  xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new_pointer(_mc_property_automaton, id, value);
-  register_symbol(symbol);
-}
-

 // TODO, fix cross-process access (this function is not used)
 void MC_dump_stacks(FILE* file)
 {
 // TODO, fix cross-process access (this function is not used)
 void MC_dump_stacks(FILE* file)
 {

diff --git a/src/mc/mc_server.cpp b/src/mc/mc_server.cpp
index 8e5f940..b869b19 100644 (file)
--- a/src/mc/mc_server.cpp
+++ b/src/mc/mc_server.cpp
@@ -212,7 +212,7 @@ bool s_mc_server::handle_events()
             xbt_die("Broken message");
           memcpy(&message, buffer, sizeof(message));
           if (message.callback)
             xbt_die("Broken message");
           memcpy(&message, buffer, sizeof(message));
           if (message.callback)

-            xbt_die("Support for callbacks/functions symbols not implemented in client/server mode.");
+            xbt_die("Support for client-side function proposition is not implemented.");

           XBT_DEBUG("Received symbol: %s", message.name);
 
           if (_mc_property_automaton == NULL)
           XBT_DEBUG("Received symbol: %s", message.name);
 
           if (_mc_property_automaton == NULL)