include/xbt/RngStream.h
include/xbt/asserts.h
include/xbt/automaton.h
+ include/xbt/automaton.hpp
include/xbt/base.h
include/xbt/config.h
include/xbt/cunit.h
* with the MC.
*/
+#ifndef SIMGRID_MODELCHECKER_H
+#define SIMGRID_MODELCHECKER_H
+
#include <stdbool.h>
#include <simgrid_config.h> /* HAVE_MC ? */
#include <xbt.h>
#include "xbt/automaton.h"
-#ifndef SIMGRID_MODELCHECKER_H
-#define SIMGRID_MODELCHECKER_H
-
SG_BEGIN_DECL()
XBT_PUBLIC(int) MC_random(int min, int max);
XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, int(*fct)(void));
XBT_PUBLIC(void) MC_automaton_new_propositional_symbol_pointer(const char *id, int* value);
-XBT_PUBLIC(void) MC_automaton_new_propositional_symbol_callback(const char* id,
- xbt_automaton_propositional_symbol_callback_type callback,
- void* data, xbt_automaton_propositional_symbol_free_function_type free_function);
+
XBT_PUBLIC(void *) MC_snapshot(void);
XBT_PUBLIC(int) MC_compare_snapshots(void *s1, void *s2);
XBT_PUBLIC(void) MC_cut(void);
#define MC_assert(a) xbt_assert(a)
#define MC_automaton_new_propositional_symbol(a, b) ((void)0)
#define MC_automaton_new_propositional_symbol_pointer(a, b) ((void)0)
-#define MC_automaton_new_propositional_symbol_callback(id,callback,data,free_function) \
- if(free_function) free_function(data);
#define MC_snapshot() ((void*)0)
#define MC_compare_snapshots(a, b) 0
#define MC_cut() ((void)0)
--- /dev/null
+/* Copyright (c) 2015. The SimGrid Team.
+ * All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef _XBT_AUTOMATON_HPP
+#define _XBT_AUTOMATON_HPP
+
+#include <utility>
+
+#include <xbt/automaton.h>
+
+namespace simgrid {
+namespace xbt {
+
+/** Add a proposition to an automaton (the C++ way)
+ *
+ * This API hides all the callback and dynamic allocation hell from
+ * the used which can use C++ style functors and lambda expressions.
+ */
+template<class F>
+xbt_automaton_propositional_symbol_t add_proposition(
+ xbt_automaton_t a, const char* id, F f)
+{
+ F* callback = new F(std::move(f));
+ return xbt_automaton_propositional_symbol_new_callback(
+ a, id,
+ [](void* callback) -> int { return (*(F*)callback)(); },
+ callback,
+ [](void* callback) -> void { delete (F*)callback; }
+ );
+}
+
+}
+}
+
+#endif
register_symbol(symbol);
}
-void MC_automaton_new_propositional_symbol_callback(const char* id,
- xbt_automaton_propositional_symbol_callback_type callback,
- void* data, xbt_automaton_propositional_symbol_free_function_type free_function)
-{
- if (_mc_property_automaton == NULL)
- _mc_property_automaton = xbt_automaton_new();
- xbt_automaton_propositional_symbol_t symbol = xbt_automaton_propositional_symbol_new_callback(
- _mc_property_automaton, id, callback, data, free_function);
- register_symbol(symbol);
-}
-
// TODO, fix cross-process access (this function is not used)
void MC_dump_stacks(FILE* file)
{
#include <sys/signalfd.h>
#include <xbt/log.h>
+#include <xbt/automaton.h>
+#include <xbt/automaton.hpp>
#include "ModelChecker.hpp"
#include "mc_protocol.h"
#include "mc_ignore.h"
#include "mcer_ignore.h"
#include "mc_exit.h"
+#include "mc/mc_liveness.h"
using simgrid::mc::remote;
mc_server_t mc_server;
-struct mc_symbol_pointer_callback
-{
- simgrid::mc::Process* process;
- void* value;
-};
-
-static int mc_symbol_pointer_callback_evaluate(void* p)
-{
- struct mc_symbol_pointer_callback* callback = (struct mc_symbol_pointer_callback*) p;
- int value;
- callback->process->read_bytes(&value, sizeof(value), remote(callback->value));
- return value;
-}
-
s_mc_server::s_mc_server(pid_t pid, int socket)
{
this->pid = pid;
xbt_die("Support for callbacks/functions symbols not implemented in client/server mode.");
XBT_DEBUG("Received symbol: %s", message.name);
- struct mc_symbol_pointer_callback* callback = xbt_new(struct mc_symbol_pointer_callback, 1);
- callback->process = &mc_model_checker->process();
- callback->value = message.data;
+ if (_mc_property_automaton == NULL)
+ _mc_property_automaton = xbt_automaton_new();
+
+ simgrid::mc::Process* process = &mc_model_checker->process();
+ simgrid::mc::remote_ptr<int> address
+ = simgrid::mc::remote((int*) message.data);
+ simgrid::xbt::add_proposition(_mc_property_automaton,
+ message.name,
+ [process, address]() { return process->read(address); }
+ );
- MC_automaton_new_propositional_symbol_callback(message.name,
- mc_symbol_pointer_callback_evaluate, callback, free);
break;
}