From 68be5601ff3ff82d68ac0368fbe2f003f9da9143 Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Thu, 15 Nov 2012 17:13:57 +0100 Subject: [PATCH] model-checker : create subdir for chord example with liveness model-checking --- examples/msg/mc/CMakeLists.txt | 13 +- .../mc/chord/chord_before_dsend_liveness.c | 965 ++++++++++++++++++ examples/msg/mc/chord/chord_liveness | Bin 0 -> 101156 bytes examples/msg/mc/{ => chord}/chord_liveness.c | 2 +- examples/msg/mc/{ => chord}/chord_liveness.h | 0 .../deploy_chord_before_dsend_liveness.xml | 31 + .../mc/{ => chord}/deploy_chord_liveness.xml | 0 .../msg/mc/{ => chord}/promela_chord_liveness | 0 8 files changed, 1004 insertions(+), 7 deletions(-) create mode 100644 examples/msg/mc/chord/chord_before_dsend_liveness.c create mode 100755 examples/msg/mc/chord/chord_liveness rename examples/msg/mc/{ => chord}/chord_liveness.c (99%) rename examples/msg/mc/{ => chord}/chord_liveness.h (100%) create mode 100644 examples/msg/mc/chord/deploy_chord_before_dsend_liveness.xml rename examples/msg/mc/{ => chord}/deploy_chord_liveness.xml (100%) rename examples/msg/mc/{ => chord}/promela_chord_liveness (100%) diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt index f0102a72fd..7f08a4c91e 100644 --- a/examples/msg/mc/CMakeLists.txt +++ b/examples/msg/mc/CMakeLists.txt @@ -4,6 +4,7 @@ if(HAVE_MC) set(EXECUTABLE_OUTPUT_PATH "${CMAKE_CURRENT_BINARY_DIR}") file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/test/") + file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/chord/") add_executable(centralized centralized_mutex.c) add_executable(bugged1 bugged1.c) @@ -12,7 +13,7 @@ if(HAVE_MC) add_executable(random_test random_test.c) add_executable(bugged1_liveness bugged1_liveness.c) add_executable(bugged2_liveness bugged2_liveness.c) - add_executable(chord_liveness chord_liveness.c) + add_executable(chord/chord_liveness chord/chord_liveness.c) add_executable(test/snapshot_comparison_liveness1 test/snapshot_comparison_liveness1.c) add_executable(test/snapshot_comparison_liveness2 test/snapshot_comparison_liveness2.c) add_executable(test/snapshot_comparison_liveness3 test/snapshot_comparison_liveness3.c) @@ -26,7 +27,7 @@ if(HAVE_MC) target_link_libraries(random_test simgrid m ) target_link_libraries(bugged1_liveness simgrid m ) target_link_libraries(bugged2_liveness simgrid m ) - target_link_libraries(chord_liveness simgrid m ) + target_link_libraries(chord/chord_liveness simgrid m ) target_link_libraries(test/snapshot_comparison_liveness1 simgrid m ) target_link_libraries(test/snapshot_comparison_liveness2 simgrid m ) target_link_libraries(test/snapshot_comparison_liveness3 simgrid m ) @@ -52,7 +53,7 @@ set(xml_files ${CMAKE_CURRENT_SOURCE_DIR}/deploy_mutex.xml ${CMAKE_CURRENT_SOURCE_DIR}/deploy_random_test.xml ${CMAKE_CURRENT_SOURCE_DIR}/platform.xml - ${CMAKE_CURRENT_SOURCE_DIR}/deploy_chord_liveness.xml + ${CMAKE_CURRENT_SOURCE_DIR}/chord/deploy_chord_liveness.xml ${CMAKE_CURRENT_SOURCE_DIR}/test/deploy_snapshot_comparison.xml PARENT_SCOPE ) @@ -67,8 +68,8 @@ set(examples_src ${CMAKE_CURRENT_SOURCE_DIR}/random_test.c ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness.h ${CMAKE_CURRENT_SOURCE_DIR}/bugged2_liveness.h - ${CMAKE_CURRENT_SOURCE_DIR}/chord_liveness.c - ${CMAKE_CURRENT_SOURCE_DIR}/chord_liveness.h + ${CMAKE_CURRENT_SOURCE_DIR}/chord/chord_liveness.c + ${CMAKE_CURRENT_SOURCE_DIR}/chord/chord_liveness.h ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison_liveness1.c ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison_liveness2.c ${CMAKE_CURRENT_SOURCE_DIR}/test/snapshot_comparison_liveness3.c @@ -81,7 +82,7 @@ set(bin_files ${CMAKE_CURRENT_SOURCE_DIR}/parse_dwarf ${CMAKE_CURRENT_SOURCE_DIR}/promela_bugged1_liveness ${CMAKE_CURRENT_SOURCE_DIR}/promela_bugged2_liveness - ${CMAKE_CURRENT_SOURCE_DIR}/promela_chord_liveness + ${CMAKE_CURRENT_SOURCE_DIR}/chord/promela_chord_liveness ${CMAKE_CURRENT_SOURCE_DIR}/test/promela PARENT_SCOPE ) diff --git a/examples/msg/mc/chord/chord_before_dsend_liveness.c b/examples/msg/mc/chord/chord_before_dsend_liveness.c new file mode 100644 index 0000000000..39962e487e --- /dev/null +++ b/examples/msg/mc/chord/chord_before_dsend_liveness.c @@ -0,0 +1,965 @@ + +/* Copyright (c) 2010. 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. */ + +#include +#include "msg/msg.h" +#include "xbt/log.h" +#include "xbt/asserts.h" +#include "simgrid/modelchecker.h" +#include "mc/mc.h" + +XBT_LOG_NEW_DEFAULT_CATEGORY(msg_chord, + "Messages specific for this msg example"); + +#define COMM_SIZE 10 +#define COMP_SIZE 0 +#define MAILBOX_NAME_SIZE 10 + +static int nb_bits = 24; +static int nb_keys = 0; +static int timeout = 1; +static int max_simulation_time = 100; +static int periodic_stabilize_delay = 5; +static int periodic_fix_fingers_delay = 12; +static int periodic_check_predecessor_delay = 12; +static int periodic_lookup_delay = 5; + +/** + * Finger element. + */ +typedef struct finger { + int id; + char mailbox[MAILBOX_NAME_SIZE]; // string representation of the id +} s_finger_t, *finger_t; + +/** + * Node data. + */ +typedef struct node { + int id; // my id + char mailbox[MAILBOX_NAME_SIZE]; // my mailbox name (string representation of the id) + s_finger_t *fingers; // finger table, of size nb_bits (fingers[0] is my successor) + int pred_id; // predecessor id + char pred_mailbox[MAILBOX_NAME_SIZE]; // predecessor's mailbox name + int next_finger_to_fix; // index of the next finger to fix in fix_fingers() + msg_comm_t comm_receive; // current communication to receive + xbt_dynar_t comms; // current communications being sent + double last_change_date; // last time I changed a finger or my predecessor +} s_node_t, *node_t; + +/** + * Types of tasks exchanged between nodes. + */ +typedef enum { + TASK_FIND_SUCCESSOR, + TASK_FIND_SUCCESSOR_ANSWER, + TASK_GET_PREDECESSOR, + TASK_GET_PREDECESSOR_ANSWER, + TASK_NOTIFY, + TASK_SUCCESSOR_LEAVING, + TASK_PREDECESSOR_LEAVING +} e_task_type_t; + +/** + * Data attached with the tasks sent and received + */ +typedef struct task_data { + e_task_type_t type; // type of task + int request_id; // id paramater (used by some types of tasks) + int request_finger; // finger parameter (used by some types of tasks) + int answer_id; // answer (used by some types of tasks) + char answer_to[MAILBOX_NAME_SIZE]; // mailbox to send an answer to (if any) + const char* issuer_host_name; // used for logging +} s_task_data_t, *task_data_t; + +static int *powers2; + +// utility functions +static void chord_initialize(void); +static int normalize(int id); +static int is_in_interval(int id, int start, int end); +static void get_mailbox(int host_id, char* mailbox); +static void task_data_destroy(task_data_t task_data); +static void print_finger_table(node_t node); +static void set_finger(node_t node, int finger_index, int id); +static void set_predecessor(node_t node, int predecessor_id); + +// process functions +static int node(int argc, char *argv[]); +static void handle_task(node_t node, msg_task_t task); + +// Chord core +static void create(node_t node); +static int join(node_t node, int known_id); +static void leave(node_t node); +static int find_successor(node_t node, int id); +static int remote_find_successor(node_t node, int ask_to_id, int id); +static int remote_get_predecessor(node_t node, int ask_to_id); +static int closest_preceding_node(node_t node, int id); +static void stabilize(node_t node); +static void notify(node_t node, int predecessor_candidate_id); +static void remote_notify(node_t node, int notify_to, int predecessor_candidate_id); +static void fix_fingers(node_t node); +static void check_predecessor(node_t node); +static void random_lookup(node_t); +static void quit_notify(node_t node, int to); + +// Liveness property +static int predJoin(void); +int node_join = 0; + +/** + * \brief Global initialization of the Chord simulation. + */ +static void chord_initialize(void) +{ + // compute the powers of 2 once for all + powers2 = xbt_new(int, nb_bits); + int pow = 1; + int i; + for (i = 0; i < nb_bits; i++) { + powers2[i] = pow; + pow = pow << 1; + } + nb_keys = pow; + XBT_DEBUG("Sets nb_keys to %d", nb_keys); +} + +/** + * \brief Turns an id into an equivalent id in [0, nb_keys). + * \param id an id + * \return the corresponding normalized id + */ +static int normalize(int id) +{ + // like id % nb_keys, but works with negatives numbers (and faster) + return id & (nb_keys - 1); +} + +/** + * \brief Returns whether a id belongs to the interval [start, end]. + * + * The parameters are noramlized to make sure they are between 0 and nb_keys - 1). + * 1 belongs to [62, 3] + * 1 does not belong to [3, 62] + * 63 belongs to [62, 3] + * 63 does not belong to [3, 62] + * 24 belongs to [21, 29] + * 24 does not belong to [29, 21] + * + * \param id id to check + * \param start lower bound + * \param end upper bound + * \return a non-zero value if id in in [start, end] + */ +static int is_in_interval(int id, int start, int end) +{ + id = normalize(id); + start = normalize(start); + end = normalize(end); + + // make sure end >= start and id >= start + if (end < start) { + end += nb_keys; + } + + if (id < start) { + id += nb_keys; + } + + return id <= end; +} + +/** + * \brief Gets the mailbox name of a host given its chord id. + * \param node_id id of a node + * \param mailbox pointer to where the mailbox name should be written + * (there must be enough space) + */ +static void get_mailbox(int node_id, char* mailbox) +{ + snprintf(mailbox, MAILBOX_NAME_SIZE - 1, "%d", node_id); +} + +/** + * \brief Frees the memory used by some task data. + * \param task_data the task data to destroy + */ +static void task_data_destroy(task_data_t task_data) +{ + xbt_free(task_data); +} + +/** + * \brief Displays the finger table of a node. + * \param node a node + */ +static void print_finger_table(node_t node) +{ + if (XBT_LOG_ISENABLED(msg_chord, xbt_log_priority_verbose)) { + int i; + XBT_VERB("My finger table:"); + XBT_VERB("Start | Succ "); + for (i = 0; i < nb_bits; i++) { + XBT_VERB(" %3d | %3d ", (node->id + powers2[i]) % nb_keys, node->fingers[i].id); + } + XBT_VERB("Predecessor: %d", node->pred_id); + } +} + +/** + * \brief Sets a finger of the current node. + * \param node the current node + * \param finger_index index of the finger to set (0 to nb_bits - 1) + * \param id the id to set for this finger + */ +static void set_finger(node_t node, int finger_index, int id) +{ + if (id != node->fingers[finger_index].id) { + node->fingers[finger_index].id = id; + get_mailbox(id, node->fingers[finger_index].mailbox); + node->last_change_date = MSG_get_clock(); + XBT_DEBUG("My new finger #%d is %d", finger_index, id); + } +} + +/** + * \brief Sets the predecessor of the current node. + * \param node the current node + * \param id the id to predecessor, or -1 to unset the predecessor + */ +static void set_predecessor(node_t node, int predecessor_id) +{ + if (predecessor_id != node->pred_id) { + node->pred_id = predecessor_id; + + if (predecessor_id != -1) { + get_mailbox(predecessor_id, node->pred_mailbox); + } + node->last_change_date = MSG_get_clock(); + + XBT_DEBUG("My new predecessor is %d", predecessor_id); + } +} + +/** + * \brief Node Function + * Arguments: + * - my id + * - the id of a guy I know in the system (except for the first node) + * - the time to sleep before I join (except for the first node) + */ +int node(int argc, char *argv[]) +{ + /* Reduce the run size for the MC */ + if(MC_is_active()){ + periodic_stabilize_delay = 8; + periodic_fix_fingers_delay = 8; + periodic_check_predecessor_delay = 8; + } + + double init_time = MSG_get_clock(); + msg_task_t task_received = NULL; + msg_comm_t comm_send = NULL; + int i; + int index; + int join_success = 0; + double deadline; + double next_stabilize_date = init_time + periodic_stabilize_delay; + double next_fix_fingers_date = init_time + periodic_fix_fingers_delay; + double next_check_predecessor_date = init_time + periodic_check_predecessor_delay; + double next_lookup_date = init_time + periodic_lookup_delay; + + xbt_assert(argc == 3 || argc == 5, "Wrong number of arguments for this node"); + + // initialize my node + s_node_t node = {0}; + node.id = atoi(argv[1]); + get_mailbox(node.id, node.mailbox); + node.next_finger_to_fix = 0; + node.comms = xbt_dynar_new(sizeof(msg_comm_t), NULL); + node.fingers = xbt_new0(s_finger_t, nb_bits); + node.last_change_date = init_time; + + for (i = 0; i < nb_bits; i++) { + node.fingers[i].id = -1; + set_finger(&node, i, node.id); + } + + if (argc == 3) { // first ring + deadline = atof(argv[2]); + create(&node); + join_success = 1; + } + else { + int known_id = atoi(argv[2]); + //double sleep_time = atof(argv[3]); + deadline = atof(argv[4]); + + /* + // sleep before starting + XBT_DEBUG("Let's sleep during %f", sleep_time); + MSG_process_sleep(sleep_time); + */ + XBT_INFO("Hey! Let's join the system."); + + join_success = join(&node, known_id); + + if(join_success) + node_join = 1; + + } + + if (join_success) { + + XBT_INFO("Node %d joined the ring", node.id); + MC_compare(); + + while (MSG_get_clock() < init_time + deadline +// && MSG_get_clock() < node.last_change_date + 1000 + && MSG_get_clock() < max_simulation_time) { + + if (node.comm_receive == NULL) { + task_received = NULL; + node.comm_receive = MSG_task_irecv(&task_received, node.mailbox); + // FIXME: do not make MSG_task_irecv() calls from several functions + } + + if (!MSG_comm_test(node.comm_receive)) { + + // no task was received: make some periodic calls + if (MSG_get_clock() >= next_stabilize_date) { + stabilize(&node); + next_stabilize_date = MSG_get_clock() + periodic_stabilize_delay; + } + else if (MSG_get_clock() >= next_fix_fingers_date) { + fix_fingers(&node); + next_fix_fingers_date = MSG_get_clock() + periodic_fix_fingers_delay; + } + else if (MSG_get_clock() >= next_check_predecessor_date) { + check_predecessor(&node); + next_check_predecessor_date = MSG_get_clock() + periodic_check_predecessor_delay; + } + else if (MSG_get_clock() >= next_lookup_date) { + random_lookup(&node); + next_lookup_date = MSG_get_clock() + periodic_lookup_delay; + } + else { + // nothing to do: sleep for a while + MSG_process_sleep(5); + } + } + else { + // a transfer has occured + + msg_error_t status = MSG_comm_get_status(node.comm_receive); + + if (status != MSG_OK) { + XBT_DEBUG("Failed to receive a task. Nevermind."); + node.comm_receive = NULL; + } + else { + // the task was successfully received + MSG_comm_destroy(node.comm_receive); + node.comm_receive = NULL; + handle_task(&node, task_received); + //MC_compare(); + } + } + + // see if some communications are finished + while ((index = MSG_comm_testany(node.comms)) != -1) { + comm_send = xbt_dynar_get_as(node.comms, index, msg_comm_t); + msg_error_t status = MSG_comm_get_status(comm_send); + xbt_dynar_remove_at(node.comms, index, &comm_send); + XBT_DEBUG("Communication %p is finished with status %d, dynar size is now %lu", + comm_send, status, xbt_dynar_length(node.comms)); + msg_task_t task = MSG_comm_get_task(comm_send); + MSG_comm_destroy(comm_send); + if (status != MSG_OK) { + task_data_destroy(MSG_task_get_data(task)); + MSG_task_destroy(task); + } + } + } + + // clean unfinished comms sent + /* unsigned int cursor; + xbt_dynar_foreach(node.comms, cursor, comm_send) { + msg_task_t task = MSG_comm_get_task(comm_send); + MSG_task_cancel(task); + task_data_destroy(MSG_task_get_data(task)); + MSG_task_destroy(task); + MSG_comm_destroy(comm_send); + // FIXME: the task is actually not destroyed because MSG thinks that the other side (whose process is dead) is still using it + }*/ + + // leave the ring + leave(&node); + } + + // stop the simulation + xbt_dynar_free(&node.comms); + xbt_free(node.fingers); + return 0; +} + +/** + * \brief This function is called when the current node receives a task. + * \param node the current node + * \param task the task to handle (don't touch it then: + * it will be destroyed, reused or forwarded) + */ +static void handle_task(node_t node, msg_task_t task) { + + XBT_DEBUG("Handling task %p", task); + msg_comm_t comm = NULL; + char mailbox[MAILBOX_NAME_SIZE]; + task_data_t task_data = (task_data_t) MSG_task_get_data(task); + e_task_type_t type = task_data->type; + + switch (type) { + + case TASK_FIND_SUCCESSOR: + XBT_DEBUG("Receiving a 'Find Successor' request from %s for id %d", + task_data->issuer_host_name, task_data->request_id); + // is my successor the successor? + if (is_in_interval(task_data->request_id, node->id + 1, node->fingers[0].id)) { + task_data->type = TASK_FIND_SUCCESSOR_ANSWER; + task_data->answer_id = node->fingers[0].id; + XBT_DEBUG("Sending back a 'Find Successor Answer' to %s (mailbox %s): the successor of %d is %d", + task_data->issuer_host_name, + task_data->answer_to, + task_data->request_id, task_data->answer_id); + comm = MSG_task_isend(task, task_data->answer_to); + xbt_dynar_push(node->comms, &comm); + } + else { + // otherwise, forward the request to the closest preceding finger in my table + int closest = closest_preceding_node(node, task_data->request_id); + XBT_DEBUG("Forwarding the 'Find Successor' request for id %d to my closest preceding finger %d", + task_data->request_id, closest); + get_mailbox(closest, mailbox); + comm = MSG_task_isend(task, mailbox); + xbt_dynar_push(node->comms, &comm); + } + break; + + case TASK_GET_PREDECESSOR: + XBT_DEBUG("Receiving a 'Get Predecessor' request from %s", task_data->issuer_host_name); + task_data->type = TASK_GET_PREDECESSOR_ANSWER; + task_data->answer_id = node->pred_id; + XBT_DEBUG("Sending back a 'Get Predecessor Answer' to %s via mailbox '%s': my predecessor is %d", + task_data->issuer_host_name, + task_data->answer_to, task_data->answer_id); + comm = MSG_task_isend(task, task_data->answer_to); + xbt_dynar_push(node->comms, &comm); + break; + + case TASK_NOTIFY: + // someone is telling me that he may be my new predecessor + XBT_DEBUG("Receiving a 'Notify' request from %s", task_data->issuer_host_name); + notify(node, task_data->request_id); + task_data_destroy(task_data); + MSG_task_destroy(task); + break; + + case TASK_PREDECESSOR_LEAVING: + // my predecessor is about to quit + XBT_DEBUG("Receiving a 'Predecessor Leaving' message from %s", task_data->issuer_host_name); + // modify my predecessor + set_predecessor(node, task_data->request_id); + task_data_destroy(task_data); + MSG_task_destroy(task); + /*TODO : + >> notify my new predecessor + >> send a notify_predecessors !! + */ + break; + + case TASK_SUCCESSOR_LEAVING: + // my successor is about to quit + XBT_DEBUG("Receiving a 'Successor Leaving' message from %s", task_data->issuer_host_name); + // modify my successor FIXME : this should be implicit ? + set_finger(node, 0, task_data->request_id); + task_data_destroy(task_data); + MSG_task_destroy(task); + /* TODO + >> notify my new successor + >> update my table & predecessors table */ + break; + + case TASK_FIND_SUCCESSOR_ANSWER: + case TASK_GET_PREDECESSOR_ANSWER: + XBT_DEBUG("Ignoring unexpected task of type %d (%p)", type, task); + task_data_destroy(task_data); + MSG_task_destroy(task); + break; + } +} + +/** + * \brief Initializes the current node as the first one of the system. + * \param node the current node + */ +static void create(node_t node) +{ + XBT_DEBUG("Create a new Chord ring..."); + set_predecessor(node, -1); // -1 means that I have no predecessor + print_finger_table(node); +} + +/** + * \brief Makes the current node join the ring, knowing the id of a node + * already in the ring + * \param node the current node + * \param known_id id of a node already in the ring + * \return 1 if the join operation succeeded, 0 otherwise + */ +static int join(node_t node, int known_id) +{ + XBT_INFO("Joining the ring with id %d, knowing node %d", node->id, known_id); + set_predecessor(node, -1); // no predecessor (yet) + + int successor_id = remote_find_successor(node, known_id, node->id); + if (successor_id == -1) { + XBT_INFO("Node %d cannot join the ring.", node->id); + } + else { + set_finger(node, 0, successor_id); + print_finger_table(node); + } + + return successor_id != -1; +} + +/** + * \brief Makes the current node quit the system + * \param node the current node + */ +static void leave(node_t node) +{ + XBT_DEBUG("Well Guys! I Think it's time for me to quit ;)"); + quit_notify(node, 1); // notify to my successor ( >>> 1 ); + quit_notify(node, -1); // notify my predecessor ( >>> -1); + // TODO ... +} + +/* + * \brief Notifies the successor or the predecessor of the current node + * of the departure + * \param node the current node + * \param to 1 to notify the successor, -1 to notify the predecessor + * FIXME: notify both nodes with only one call + */ +static void quit_notify(node_t node, int to) +{ + /* TODO + task_data_t req_data = xbt_new0(s_task_data_t, 1); + req_data->request_id = node->id; + req_data->successor_id = node->fingers[0].id; + req_data->pred_id = node->pred_id; + req_data->issuer_host_name = MSG_host_get_name(MSG_host_self()); + req_data->answer_to = NULL; + const char* task_name = NULL; + const char* to_mailbox = NULL; + if (to == 1) { // notify my successor + to_mailbox = node->fingers[0].mailbox; + INFO2("Telling my Successor %d about my departure via mailbox %s", + node->fingers[0].id, to_mailbox); + req_data->type = TASK_PREDECESSOR_LEAVING; + } + else if (to == -1) { // notify my predecessor + + if (node->pred_id == -1) { + return; + } + + to_mailbox = node->pred_mailbox; + INFO2("Telling my Predecessor %d about my departure via mailbox %s", + node->pred_id, to_mailbox); + req_data->type = TASK_SUCCESSOR_LEAVING; + } + msg_task_t task = MSG_task_create(NULL, COMP_SIZE, COMM_SIZE, req_data); + //char* mailbox = get_mailbox(to_mailbox); + msg_comm_t comm = MSG_task_isend(task, to_mailbox); + xbt_dynar_push(node->comms, &comm); + */ +} + +/** + * \brief Makes the current node find the successor node of an id. + * \param node the current node + * \param id the id to find + * \return the id of the successor node, or -1 if the request failed + */ +static int find_successor(node_t node, int id) +{ + // is my successor the successor? + if (is_in_interval(id, node->id + 1, node->fingers[0].id)) { + return node->fingers[0].id; + } + + // otherwise, ask the closest preceding finger in my table + int closest = closest_preceding_node(node, id); + return remote_find_successor(node, closest, id); +} + +/** + * \brief Asks another node the successor node of an id. + * \param node the current node + * \param ask_to the node to ask to + * \param id the id to find + * \return the id of the successor node, or -1 if the request failed + */ +static int remote_find_successor(node_t node, int ask_to, int id) +{ + int successor = -1; + int stop = 0; + char mailbox[MAILBOX_NAME_SIZE]; + get_mailbox(ask_to, mailbox); + task_data_t req_data = xbt_new0(s_task_data_t, 1); + req_data->type = TASK_FIND_SUCCESSOR; + req_data->request_id = id; + get_mailbox(node->id, req_data->answer_to); + req_data->issuer_host_name = MSG_host_get_name(MSG_host_self()); + + // send a "Find Successor" request to ask_to_id + msg_task_t task_sent = MSG_task_create(NULL, COMP_SIZE, COMM_SIZE, req_data); + XBT_DEBUG("Sending a 'Find Successor' request (task %p) to %d for id %d", task_sent, ask_to, id); + msg_error_t res = MSG_task_send_with_timeout(task_sent, mailbox, timeout); + + if (res != MSG_OK) { + XBT_DEBUG("Failed to send the 'Find Successor' request (task %p) to %d for id %d", + task_sent, ask_to, id); + MSG_task_destroy(task_sent); + task_data_destroy(req_data); + } + else { + + // receive the answer + XBT_DEBUG("Sent a 'Find Successor' request (task %p) to %d for key %d, waiting for the answer", + task_sent, ask_to, id); + + do { + if (node->comm_receive == NULL) { + msg_task_t task_received = NULL; + node->comm_receive = MSG_task_irecv(&task_received, node->mailbox); + } + + res = MSG_comm_wait(node->comm_receive, timeout); + + if (res != MSG_OK) { + XBT_DEBUG("Failed to receive the answer to my 'Find Successor' request (task %p): %d", + task_sent, res); + stop = 1; + MSG_comm_destroy(node->comm_receive); + node->comm_receive = NULL; + } + else { + msg_task_t task_received = MSG_comm_get_task(node->comm_receive); + XBT_DEBUG("Received a task (%p)", task_received); + task_data_t ans_data = MSG_task_get_data(task_received); + + if (MC_is_active()) { + MC_assert(task_received == task_sent); + } + + if (task_received != task_sent) { + // this is not the expected answer + MSG_comm_destroy(node->comm_receive); + node->comm_receive = NULL; + handle_task(node, task_received); + } + else { + // this is our answer + XBT_DEBUG("Received the answer to my 'Find Successor' request for id %d (task %p): the successor of key %d is %d", + ans_data->request_id, task_received, id, ans_data->answer_id); + successor = ans_data->answer_id; + stop = 1; + MSG_comm_destroy(node->comm_receive); + node->comm_receive = NULL; + MSG_task_destroy(task_received); + task_data_destroy(req_data); + } + } + } while (!stop); + } + + return successor; +} + +/** + * \brief Asks another node its predecessor. + * \param node the current node + * \param ask_to the node to ask to + * \return the id of its predecessor node, or -1 if the request failed + * (or if the node does not know its predecessor) + */ +static int remote_get_predecessor(node_t node, int ask_to) +{ + int predecessor_id = -1; + int stop = 0; + char mailbox[MAILBOX_NAME_SIZE]; + get_mailbox(ask_to, mailbox); + task_data_t req_data = xbt_new0(s_task_data_t, 1); + req_data->type = TASK_GET_PREDECESSOR; + get_mailbox(node->id, req_data->answer_to); + req_data->issuer_host_name = MSG_host_get_name(MSG_host_self()); + + // send a "Get Predecessor" request to ask_to_id + XBT_DEBUG("Sending a 'Get Predecessor' request to %d", ask_to); + msg_task_t task_sent = MSG_task_create(NULL, COMP_SIZE, COMM_SIZE, req_data); + msg_error_t res = MSG_task_send_with_timeout(task_sent, mailbox, timeout); + + if (res != MSG_OK) { + XBT_DEBUG("Failed to send the 'Get Predecessor' request (task %p) to %d", + task_sent, ask_to); + MSG_task_destroy(task_sent); + task_data_destroy(req_data); + } + else { + + // receive the answer + XBT_DEBUG("Sent 'Get Predecessor' request (task %p) to %d, waiting for the answer on my mailbox '%s'", + task_sent, ask_to, req_data->answer_to); + + do { + if (node->comm_receive == NULL) { // FIXME simplify this + msg_task_t task_received = NULL; + node->comm_receive = MSG_task_irecv(&task_received, node->mailbox); + } + + res = MSG_comm_wait(node->comm_receive, timeout); + + if (res != MSG_OK) { + XBT_DEBUG("Failed to receive the answer to my 'Get Predecessor' request (task %p): %d", + task_sent, res); + stop = 1; + MSG_comm_destroy(node->comm_receive); + node->comm_receive = NULL; + } + else { + msg_task_t task_received = MSG_comm_get_task(node->comm_receive); + task_data_t ans_data = MSG_task_get_data(task_received); + + if (MC_is_active()) { + MC_assert(task_received == task_sent); + } + + if (task_received != task_sent) { + MSG_comm_destroy(node->comm_receive); + node->comm_receive = NULL; + handle_task(node, task_received); + } + else { + XBT_DEBUG("Received the answer to my 'Get Predecessor' request (task %p): the predecessor of node %d is %d", + task_received, ask_to, ans_data->answer_id); + predecessor_id = ans_data->answer_id; + stop = 1; + MSG_comm_destroy(node->comm_receive); + node->comm_receive = NULL; + MSG_task_destroy(task_received); + task_data_destroy(req_data); + } + } + } while (!stop); + } + + return predecessor_id; +} + +/** + * \brief Returns the closest preceding finger of an id + * with respect to the finger table of the current node. + * \param node the current node + * \param id the id to find + * \return the closest preceding finger of that id + */ +int closest_preceding_node(node_t node, int id) +{ + int i; + for (i = nb_bits - 1; i >= 0; i--) { + if (is_in_interval(node->fingers[i].id, node->id + 1, id - 1)) { + return node->fingers[i].id; + } + } + return node->id; +} + +/** + * \brief This function is called periodically. It checks the immediate + * successor of the current node. + * \param node the current node + */ +static void stabilize(node_t node) +{ + XBT_DEBUG("Stabilizing node"); + + // get the predecessor of my immediate successor + int candidate_id; + int successor_id = node->fingers[0].id; + if (successor_id != node->id) { + candidate_id = remote_get_predecessor(node, successor_id); + } + else { + candidate_id = node->pred_id; + } + + // this node is a candidate to become my new successor + if (candidate_id != -1 + && is_in_interval(candidate_id, node->id + 1, successor_id - 1)) { + set_finger(node, 0, candidate_id); + } + if (successor_id != node->id) { + remote_notify(node, successor_id, node->id); + } +} + +/** + * \brief Notifies the current node that its predecessor may have changed. + * \param node the current node + * \param candidate_id the possible new predecessor + */ +static void notify(node_t node, int predecessor_candidate_id) { + + if (node->pred_id == -1 + || is_in_interval(predecessor_candidate_id, node->pred_id + 1, node->id - 1)) { + + set_predecessor(node, predecessor_candidate_id); + print_finger_table(node); + } + else { + XBT_DEBUG("I don't have to change my predecessor to %d", predecessor_candidate_id); + } +} + +/** + * \brief Notifies a remote node that its predecessor may have changed. + * \param node the current node + * \param notify_id id of the node to notify + * \param candidate_id the possible new predecessor + */ +static void remote_notify(node_t node, int notify_id, int predecessor_candidate_id) { + + task_data_t req_data = xbt_new0(s_task_data_t, 1); + req_data->type = TASK_NOTIFY; + req_data->request_id = predecessor_candidate_id; + req_data->issuer_host_name = MSG_host_get_name(MSG_host_self()); + + // send a "Notify" request to notify_id + msg_task_t task = MSG_task_create(NULL, COMP_SIZE, COMM_SIZE, req_data); + XBT_DEBUG("Sending a 'Notify' request (task %p) to %d", task, notify_id); + char mailbox[MAILBOX_NAME_SIZE]; + get_mailbox(notify_id, mailbox); + msg_comm_t comm = MSG_task_isend(task, mailbox); + xbt_dynar_push(node->comms, &comm); +} + +/** + * \brief This function is called periodically. + * It refreshes the finger table of the current node. + * \param node the current node + */ +static void fix_fingers(node_t node) { + + XBT_DEBUG("Fixing fingers"); + int i = node->next_finger_to_fix; + int id = find_successor(node, node->id + powers2[i]); + if (id != -1) { + + if (id != node->fingers[i].id) { + set_finger(node, i, id); + print_finger_table(node); + } + node->next_finger_to_fix = (i + 1) % nb_bits; + } +} + +/** + * \brief This function is called periodically. + * It checks whether the predecessor has failed + * \param node the current node + */ +static void check_predecessor(node_t node) +{ + XBT_DEBUG("Checking whether my predecessor is alive"); + // TODO +} + +/** + * \brief Performs a find successor request to a random id. + * \param node the current node + */ +static void random_lookup(node_t node) +{ + int id = 1337; // TODO pick a pseudorandom id + XBT_DEBUG("Making a lookup request for id %d", id); + find_successor(node, id); +} + +static int predJoin(void){ + return node_join; +} + +/** + * \brief Main function. + */ +int main(int argc, char *argv[]) +{ + /*if (argc < 3) { + printf("Usage: %s [-nb_bits=n] [-timeout=t] platform_file deployment_file\n", argv[0]); + printf("example: %s ../msg_platform.xml chord.xml\n", argv[0]); + exit(1); + }*/ + + MSG_init(&argc, argv); + + char **options = &argv[0]; + while (!strncmp(options[0], "-", 1)) { + + int length = strlen("-nb_bits="); + if (!strncmp(options[0], "-nb_bits=", length) && strlen(options[0]) > length) { + nb_bits = atoi(options[0] + length); + XBT_DEBUG("Set nb_bits to %d", nb_bits); + } + else { + + length = strlen("-timeout="); + if (!strncmp(options[0], "-timeout=", length) && strlen(options[0]) > length) { + timeout = atoi(options[0] + length); + XBT_DEBUG("Set timeout to %d", timeout); + } + else { + xbt_assert(0, "Invalid chord option '%s'", options[0]); + } + } + options++; + } + + //const char* platform_file = options[0]; + //const char* application_file = options[1]; + + chord_initialize(); + + MSG_config("model-check/property","promela_chord_liveness"); + MC_automaton_new_propositional_symbol("join", &predJoin); + + MSG_create_environment("../msg_platform.xml"); + + MSG_function_register("node", node); + MSG_launch_application("deploy_chord_before_dsend_liveness.xml"); + + msg_error_t res = MSG_main(); + XBT_INFO("Simulation time: %g", MSG_get_clock()); + + + if (res == MSG_OK) + return 0; + else + return 1; +} diff --git a/examples/msg/mc/chord/chord_liveness b/examples/msg/mc/chord/chord_liveness new file mode 100755 index 0000000000000000000000000000000000000000..b77a33df7946ad239f2486147f1a1f1d93c78898 GIT binary patch literal 101156 zcmeFad0=m_RnONO0-RHd!Q_nHdNwiw4wm zq=MCo?OVla`}%gJt+iAX<5GimL)$9dsRf%T?Ms!{qAxAq&-0vf@7xI!)Zg#>`|o#Q z=G^C;=RD`x&U2P~=VY6wyws+uigDSLl?p+Lv)!B}z7=I}dl<*9rmCY;FCjzZ>e{#J*IJw@yoa{p5VZef&APhx!Gy{-n2~SKM{ne$<>whOw!QDrGSXf8Ti=oq4Mvq+q=*H*YdKD zuKm-|2Yys{saF2`?-rwsWSx%Be0=D-1fMzhOeO%AhR>CBgX=1MsErl)tioqGJ`3<6 zf0%;LB7BJVdHB%f5{W|X(3OGD#rP0k+4xwmg#gml_F85BF&NaMnZO_D_$f@0n(ZHHjUvylPk#H! zhrI>wh33Z1c0HXa%9%TP=-I$bD>mS3wz&wp+LI*k+XbI%0yeG}0Cj|uW~CTMs11o%%) z&~D8He108t$cM&XJ0`$Sn1G*M6Y$eN0iByB$R}Ub#xp~C6VO*C$bWnSK0iM}e$52= z7f+C%IRXD4PQcHt6Xip;Xnr_0K|b|W4WIE><^=R#1Y$J$H%)-QcmjEUJ3+p00zG&q zp#Rcgc3g^SN5Kdu*J3)=T=%aqS*L zKI!L3xtr;tI$t{4rTh`8HyYRJN|E`;B>s@dR+41CF+Y~sN&@n=DEuFl?asZ#&8Wt_ z<&V<7+a>?il28HYOrsgnxO@fkG=FDzdw*vuP0q5?3KYGpu0n71_50d8{Q+NpT}5$M zZ;!98skzIi=z4p1Z;$Q|H1!8`UD4NU)N3SOaaWVy@AHf5Q7c!}uGRxh{tbF(zprJZ zLSRd8cQ@Md2l{(Ab4FKFu&1R%Z|dvo>TGEWboTb3&4K2C?i+x-(lD=MlCsl6h(*2ven|r&Mcz08058rh3`UAS(*VPtg zqTLr@=E6Avu*DFy8_B?xwD;-WH}p^0olj0RDpgZF+03-rd{k z>(W~~e8?n45mCLTH=MzKLt4={bp|^0KxenFHyBV_!c^Inh%}rt5cD${uGPZKkfV2# zi|5i^A2QkB2?+LV>g;KyC5kSVD0!6IA0UJb#tw9V26vEj1)ZV&rtUt%J(1rRHIAt4sbt-L!YIUk9yAXS%zsD%@vAgJcGkF{JF$FqoRhD-2 zcKeogH}%6-OKU}Mr3Du3&a_(mLA?zsQ+l9A{ia@c`2^n5($U-Bib}95c{KW85BLqX z1bX|aJF~kQEtgf{uC=pA5Bhzr)~49vpQr()uiw|YhWJ@sURG4BXQpMQ(aOMPF3%}E z88K6YDuP5#Bo>t-=ta3A>#LaZ82<=a+!IYBmr}9v5~cG&mew#DKEX>nv3#^E9f+57 z5$-ZsPOvDqndN=Wjg-x6dF%Smh_lp^u|6U^BQDe0tB5k>WsJv^Piqq6GR8m3x2~y< z$v95=v<5RTIX+Q7twD{;7`G^&*1pEITk<~%8N{n`?X~1v^}ElKFIB`FX)TR>OZl{Z zHZE67Bi~X!?Nb<6dP^hUQogY!ri}cSMoM^1O#3Frw(bv*Q3Ad~9o%kAP zY2+Kizk=_?*Y=i1zM=eNz7t<}w>0t%z#75F7=Djn>N;ab7=DM~`2-I${1(B<1n+0~ zw**ty8QaJ3>jYDm8Qab9s{~V58QaeA3j|Xa8S4X_@wc*}*FNJNddoX_{8V*a*~l=h zn7kv;(?ZBQGD7Ri(RMI?diQSfX>Z7pvPM(9JBI_db4S>@cU!Lm+gclydhe0}B;LU@ z@!p{mn`}3}cmVBjrPDV)M@8q3CCuASc?SqG@Si_p2flac1@H6ktn#WyyhAU0U;B3u z^`9nO@6Oi)M*X*B{p~9Xpid<@tsXT;w?d&ezU)|tEcN{tsegF~S7@t&5SU}KFs=T% z*^S_C=)}1rH;&zkDq|b*wR<;_2sv!f&(7gs!Xf0HdyeJ{qyIb$vM*9GRL~c4Bml*` z*Zcf2n|H`_${WIGXk_$JXbJGBcW}$766_8+@&%=&LzBS#b2P&k{T3)eb!$V8c_fnVJyaxKJn-EZe;K8qU=!pDeo@N?n7s&Y-og~8C?krj{fL> z(QXLs4mnnW=!oYmMUN5B8GI}6YOvTMWQXd{cw1igKL3`@tG*EOoE@^g<~uv+IirRg zZWy${bLO^RQ?}y+GH=L{j3nfCK@+n9%>;Caf)EKhiUuJ>9rFKGMp&tXXKdR%0RIlq zJLK67Sr{3zXqDg>vK$ez>;jF@%=@SflI8{~HKgf-a$XT?4mtdUg2t{#V?y^sTh4|Y z4agoGRg*nuO@kz&U?_NIsQxtZKQej*b{q1X4SCK0c#(lKA3g-TO|so*wT z!8^3&3{cOI9JL>jcZ`gND3y8V$a2z9X01Nd+8c7*>SZ^)m^LyL;f8&vx^p;TM-_A% za(o5|gJ_x*sw25SYxRjJK9t{A8URykwAVD@dR0ImQCgYAQXs2wn~UmEPd zem2QaJvNt`%86qM)eNA}PQ&wn)UpZ{j)Hw`&{ zTuNQZ7E2odNy<9eM*E`CsVj zqm59*dkND>zx1hp!aG!y4|$&OSe5WaKxXLa{-+sw?qDo4^!Ncn3HwJp2hbnLlZT}z zAKu5FeB=XUhbs1k>K}&=_8Wn7U>m^pHUIJuF_236A)isd)n~cR$6#@J*zzL+sR3)~*|R)C{ooXmkmFU5Mijq%#NovqO#nw6Mdsbr@^17X$UvN( zqf|E}k|EDw=yxxw7{g4+F$opkOISSoUP6QCFv&j}a{RM+T;8#ej?X(X z$h_JUc6@|31mH;6@izcaiW5y??lI&Ue(o3~7DM4<|3m!M55tGhEj_~{?%BkjxaAcP z-L{RmHIeBZak~g%bXmA!I*1wIq``&NB6l6y4;4nfFE{ zCmc3*HlhM<4}-D0T^blG<-}x~S6B-6RM;!M7GTPWSb`8TW28}fkW61Mln7Ag1H%&l1wV$P5)-s06Jy!i{ccEDjYEIr;&5hggpztbAKo`63ds^2uj~@;xe)FBQMks`yc~ z5vqUE(AyiNw`ZmxfOyUfZaJeQ?Dztk&7m*@#uV|rRbVrQN`U_3e=wVE;On=@=P6>$ zwsio10x*J2t|ELSDw}J-rm&^K>{=_c%fal3qX4V`PZ9im4Re{X)%fy;Jlm<)Ei}TF zl!?Y7?=B2FLoD2Xo?>_3&gkI&V&*FVVTwOy~rm@FeA<6&Aby?7vO-d<*%~?&O}o1o)}!zKI%>?%86sco|uXSb`b;@OSE5 z`vgU(I8=5fYC=N7%@0f3)Mdv}7p$X@e=l}U$%$pQ< zFGmABd)oh1vSO%yJA%RPLvL6$^cPSy1bFZysRQdctlL5egQo|#oQ_SnYf>z9>^bcX z#r$}74Yu-*p~;iWtbG0vkjdwFK?Qu?2&|VGi}|Dl(hmWGezaw?RI}2Vq3SsB zlpG<*OsgQH@3J8M!1`AKiOYht0Q@_^3k&j;A;&$p?&?W%yYcp_wY?;XhS zBoA7SujO04XfGg>*9|~}7hMbHwlfwhe>K3H0eUa!MK4KSP4_us<@6t*O!^z)$9bee zS}r0(IK=b_o?@&#y*b7_b%2SJd8R|G2lxko7v|{|Lw|kj5YoC9PdIf*xrPia-C(Wc zGMXEF2Yig(%p;bgg&8r-T@T1qp-Zq!DqIm}msFVcvF!e0yb2qv%zYb_Nn;_a3l7d= zzuZni?k#lDF+s!ee6H2V-v?xJc;~2TmBYAb9L8XN0JfP! zH*vUxX*lLZa5&A%;qkwk9DbN%nw)g_4!{d@_||w14_G<839?&scnFaS^so^~{YEnR zCB%ZUyE%qAZsFz)Lw5l()woJ9Nn0j$VJ2zI#PhLC{tZlq>Ji*4#NaS$trLwEUcv*$Fr@*eFKom)qlOss-wVvh_TqXs{nonpf~y+M)!J5+dW6k~-X!!mtt3K}pWOBRy1naX8SUrpdea38S0;mJ@ijA=exJ@E% ziODZpnfxm#zN?9S-o2&+{#Fb?STu}`RwD`#ZwU`XY!MsQe>>C4?NLCc^}li4wEi$- znb!XtZZ6-1Pv@q?6%Typf%x5V8WaL<*5hT2jchY{cz(WJDo@oO4Od zjMlh8MhYBosE@`F8?=o^56tlJYD7VYAEy^&579ts zaRiZpD!a~egliF5M*l^=1hv#t8mb?ajxcJhaxd%%_i}B|G1zp$QmZ4(0%SS@J*S5w zv;*tkX@td&K$FM+2KdPxp(N}Gye}{MhgNIxg3mxpSPOzIdjVND1op(#b{Y!Jz^-B3 z86659CtaFT`B9$#hdjr5?*B6pd1#s?P?UFFp?a<%2(H0i7CkttKTf-5qKjXKd|m(EcUxrfSUlq??|)}?kq9@kv?PqB7L|i z0C7~Jx6?yEa3e3Yi_Jt`Md*gsT@6+r{4JUdIW#n3@j-Mf-Z|Ta!XeM`!7azJ|MGR# zm}BfJs|ddXWQy?ZKbRuC$XKQbPXhc@A_Oli!d|Ng7YpNp>5deNul^tKCgdd$jcH=0GjBmY7#PWPfOEJ4qCLO7$y7kif&?%4wG{*F)| z;2J|k=^@9)#pak{l7ZaGzqeTGps>^`poYw6{272uOT_?P2DwWZ%M5ZC0sK^!x|`&$ zK%6ms>`;E48#Lrlw;4?#aA0Oj@!!hxBPcPlM%?M7gt6c8;voX<45?tqa}*ZsPO(a) z12QGb1QsNs{<4~}SRz^*7>fn$1-K62 zrxNgMETHE|h<9m@U^y$I1y)0b&~l4ruT}K#khmdKbH`yEiEh)MFwQuMg|>c-ZYnnL zKRk<=<2h^2WX~IQErT!jmy!qo%wnuopd0^3bfPZk{1i)rVQ<`gJ0Ds*f4Fmz1eo{X8T6G=N0mH~ zGe?z2h2wu7sNq<(6Obuq!<#H8&CI(Qi{+%5`DXxrDmi~fa*iJo52agWeHE?2ay*zM zAwZ4Ai^1f*1y%-+12P%>;Tz0g5FGuKv6w-!%d-GK6@$MLJrfg=zQpqwEyLK|XXW*B z<~1BFKYlp*k6)8?mf>U(IFw5eYiRxz@JtiQ;p9}ZRReDUGBxl6pv&RpRmNfs(46@o zz)z)tV>Xy5ayU6+m3c9g9X<3^qr`~6#&ELw{Nd!kNCiBch_Lj~uNa;`IfafWXo}Fi>tEK;J$O=+3zLxJH&-B>j;a_L-mS)(1dDL$ zM#duwu_Q5Gq{2&9c#(>iEwe-v!;2Gg*%I+0mhx`mVE0)Sdojx9uM2wSny3#=?}g?X z&~P|(tN~=I`?6oMx@j*ild)Lcs{keg^bUDwrwe+-az4D%l|W(9Gd#zR>|LIHhqhZ4 z`3+D6A7~fvjA1!-hJX;>nmQAhMLQF;!^IP~D?X$iboSkg7{NUo_q3xF$ifzg&<(2L z@eRGyNRMvfMUrc)w|{RnbMSo6FzZPwpcV4Lv)6@n+};0s4NR58trb zsEdl=JLV3^Z;o((K88i-F@8^XH<%c==yV8<@t*D`6w)NX4O-iI2H?4S5|PAfyYfBV zy<)3tpIl{PCFR*3xy1Ye$c;{;c6s@3>~qBk*3N{OSu8O}S3oGz>I0~NL4LxGtPVM_ zQW{=I{(@?WjjYzot=6~}kZFw+@PQE10QIkAEVc$c?OF;D^|z0BXwJ?eishqc@8289 z=l9Xi@k6^v!8`>aK@VGv@-32aSN)ODPR8K{^0O3Lc2!XPJY{`orvle>OQWxT^D-;n z4+Ap!zWEnsU%ivD%)Yt_Aoz~fSKng3hjpW`zHjCB94LaTy$BBIeSDV)HJl;p*a2yI z#ryo9@k-}mywdpsl?w0wEWdL=ufm+8$8fT%M@A*;?$|&+BQ{dxp7ujL{?J<|BclmW z3VQb7uo{{=JXe$NihjtgRJ%;IG*WK`OAi1g9K!AbWUA%5pPOpwWh_%IjR2vRXr1c_ ztL2DasAc~l=Q=k~c+SFtX{96J9eeIFfMZ<7R0hk=e^Xh!`3D2u%$+?zt2y4LPUFvolt<;A>IW2ck#QAc9f1AD1QH{=zSqaB?@VvD5jA? z3>4-MI%E`mLaOyKv?c7G$caB3b3wi0+H6%5kdyJ%^& z6rdP4QfC`lo(+e(9FX~(?H|CzxN$S`V;Kt?j@i}>@Shi(+T|e)1I0Lr4?yD4KD0t_ zQ_?8y4T)q|{ccQZDF^FBP7i$6mK`ufs3WK$KsZX8RX@z3)4_y(=FO}nxys5NiKc?w!vQ)d@`OpY^`qWz>@w(MWp z?QdV&-LjOK7T@M?*3(*)T3^7g^)%}ne4G7RpjW%HRl)y?%^H3K-|mAHbX3JMrIvm` zuid8A23uM*MY}SqRRctcQjMRb`{+!E-u`7&9d&VVgi$~F%2o|}2BsocGwVZ~Q!ueYyuQs>Xyv}ZBELpI--jW58Z;a5 zb*CwnpaW*Oz}Lz}IHaLnDb#QTMUTG?40JU4wcZw-Md2ge(pAceChg#?4Ih5*uQfq0 z{tanbC608Ub2M7h2(JzeQNFebB>d16l+qUL>e_77YlY=B5{2~PZR%;od2a2Z%9VYJ zQp40Kt4Ui_3aYGb*6bpXxH*VJG_}QQ+{B zfCf{y__(@sCSn#>gq*8=0nOq<=Lrh@@$!wUGETsaolTk{aO8x}9 z1UC1vH9obZ9}D&4rasi&tm5bkMAN#Sdqud7R29o+1{LMzki zIy!qcXr0t6>A(^0+DPCrHwQZd+Hy!`*cskmUE?Y76nkoGt7`OePvNy?m8;o-VM^Jt z;B(TQto3T^i=)@FIzW_q6ZJM1>mNGj-qXrl%U)-V3v`$Yt82nOav?&HJ8*u#4ZC8r zx`@}1KNX<{XY;@uB2pqUac39$KR<4fMFocJsvplU$8^zS;f^BkX~GN5+)qxH*c73{ z6e>y(62ck7gVny{x_($kV(1z#ci1iyRy6q#7A6X8k42xf#zZ#IdV47HSVNIuFUojw zz5+kKbv6uBynr1(2^nhK+C30$WapL^z~JB9+0}WA(e0%eN}1N$+p{Qu5feiq4A9ci zggL|ba2vJ^^va_F`uF%~JKhSVodfLE_`*q0vcY0H(ulG*b@;$^|M-?L&uF6Kcntn3 zni#uD>+0>@5bO&Np@tJm#L~jL!g9@1Q&Uy5Ok3X@?1wsf+xwfkc_7DGNPRTX(l`p@ z#GutU-%FDRRG|;1@&8oxD-HoY8V2odbv&o&L0o zlqHyfHFpO5E8u$pnvM}59de00pGlNSK$eyDY=p$E&^!h4-aa~jN~1v!XPQEWZeLdu z4uY~CQ>5_eP)qnQsHJqcm#;stS>a=j($bdVKcQL|B5js{wBNR}Li6&iMoR$vgg4QoN3 za0ORx?ed9J%&0e*#Bk#u*AT&idx6C#P{|xnptIg0E@2Tm`Kc4uyG0zqCeQRz=h&Ci z`~CA!LZPL8TFC=2>UCKBkjgBf|roSVXx~r(hb-ijPVVLFGH}Sqy#8L~7Qr4%dGi+4C+?{u0V(pq$ro27Ox#6CnD>@woxz8Awg~U19n$ zkhdG~UAHQ(!+%K*4Z9g~5 zcc6UW#dGI=KngSI?{^yXA4mCA>?S=)?|qu(--$KKUqbn#*cg8#g8mmx`o~eO;jxR3 zG+h5WQ~xoLOUHie=OXG4ne`W-{AVaX34aUM|Et|-zXatE;VINa`fo+~pHaRsg8!RM z{&%1}?@#B>9duafKjkp!KaTR(@rvB75&Ug5`FjcFOYny4%n11sP5F+ad_LZOd?TX% zYi9iz$aNIu&qvgM#;m^p<(tv(E{-UlZkCszybr${xFdr87L$G}%3nwMmm|ven&mrC zUWI-fXDwgN#q3{?qkK8a`3zIj{{O@Jr~dmA%4eg0Lrn8pfVEUt&9&BNSFCGWe zS$@`XI=hdq1d%9Tl`#7V@{IFqr^<5U{M$<;Y@FjiN5Y9Rz0`mk8~Kjn7hM#3=rY`* z(dGuEDF5^CbG?+_9pk2i-$JJJi79SM#NQA=>UFpYR4(FgoF^m+O_A_ynR1Mm_moJn zF!yNWT*HTlWq~n1(IZ8=E*6RM#56bG8Tq4$0yg9r=F;$)`bPWzJ}2aPLgJs3u+i=* z3D1?~lFa|-iShRn#y9kZnQqSdnoOUP>B};GL#A)b^aGj3&Jy)z$#kJib7fj8(`#kg zCew{Fy;G)Nkm=WC`jkvxmgyTZeOsm<$Taq1*}hB{$~0G|r82!%rfo9aDAPM-`URPO zO{P!D^ktd8A=9^I`hiSi$MsuQ;{S`U-4#NfeKI9d@SSr;e;-fU%x`VvBJ#gXd`98d zGms9*5A~PT#l_1sSBbB=v#CeRPRmQnSdy0_ZpN3PbV&x4;fDXlg7916^+xRaZWf3} zxwc_Ykof9D2pnoVxOlY-leA0RjQ+E7ks5VvquJ=8zrGr<-8t!c#1^~ieC-A#wn?+F z(6Gl$dTS45#_m8rwA&opKZ^(woJ2o>PS$#QRd8D4TMA$)fHQ^;v8H8aHjfs2A$47>;^bXf{D(%iveCN z!P(By$pB|dP;++g1$c=BUCz!LfR{=z-Fa{wz&R4kcgAf8I9Gyh=K(0nak&J&PWwiH z^CVd9+>I%XLz7^GQ-g^e^VKOZvMssM`2nK0V}Ux2!478|n0G9c67@OnEdsb$f&u40 zN#0ZyIz!z7=j({rj&yYmKzs6b)p_Vnz!_=-!*{68Bw{2}rE$cbJg7Q{5osN{>LP~k zR-OM#bs30@=NCsb!E!D}VFUv+LExLl<< zv_1KN>U`%jfGe4Md-AaA+*AU%T3y2JV@7J*T#V7dH2_mirne>Na}nGF*OY2F=90N*Jrv3)In2sl>_-BKb<7rZP z-0$Gej)Ow`O5C@I<7b5OopIk=3TRk(Q=$^O|lp3B*r**g^`;C z++qOngljwbDEzaUyfh(Z@{+yCPuy04g2W#$M6XJG9TPoU;(koK?1|?};q!@KxdV+S zo^qqf#M1Q;Bk=>6%b6I0@Y@vIU=G?_Rtq}Qd?2dYSZinK$Ih|N$0++VTPb_@65xIK z6V9gR?lu>O@5vw0Ja1C|bVaG2oTxTo;GK^1t(D2s)OnatQ{S=g0NQkw7=!D*?;_ne_?1`@wlLJ4~N)EhWAvy4Ags4f0 zG~sn7y2x`AkE}$4iOuzpAn_c$DNdPn0}A4&s53zN;wR!0)neFqI`+Gi_-Qg)D$X|_ z1kQAonkToM>jyYPnj_BnjhO&vso)f)iOxB<12jVVZ0C+y0F4-~O{W9gAAGVf{{4W^F@=k6)l}A~_GlFIK;RGUpO%?<&5h?)OiqDn3>H4-}D{cdr7tM17P& z3Pog~*=-;^n<&pZI}PP&s!sRY=Hq^uN+)E-I$y$flKLv&e~n5Xfg8lHQh(1mZ{hnA z_3!w;l)ivZ)MA}P7=!Tx<&;bcV7RyaHAwoM>e8dQp9ur2 z=_CvBlY>5_W>CH@IYxx)Q2^2?wxeKI&D>8U_H-zUTg~f*cQc9n2oeR7MBKmO!Rj)? zf=F@SfDfz71?KFybZYEsfjKv>gZN${%3N_vsou(VW+Xjs4cty$Rl%N<58V<^wjMZx z>VBVY`}j75R$`r$kr1PLUILW(Wpq0w@fq|7HF57&U?yGz_1Y89>?6he8y@LMTyhtx zDYlrqfmE>vwWb_~9b9TnI_8jZmr~tYB1ZbT6ZOjso`BWW1~D*bif!&Tfa`xjL@(#tQZyCoq>MR_+=JX^F+cbZWY6sZm;o^^ z>-YH;TPyfiF2DCuMfoNQRl=U9?dwOKE*ha!b>0;ZE+*(T^gdiX+!89=@FFFiXwG@R z6exbth>8)D8u5o437U;eL!nC8vXRXZjcm3yLa5xx6eXT$&R37$iOO?SV-~#p5;wC% zUur2ZG)E^P2$D+j?p{E5s0P|sE*0pFgq|0Nt<%2VO^SLaYj{uBf=)%fOWb!{N%~j~ z6m_zl&U>Y6VL1e?l}-Lmrs~d_z*=-8ifnrtUE_;W+PI)0RRZ-G&FhHq?4O$#f4s*EM z)2JkW*oeZ{RHN3HWNkOKxSnc7U+*SV#r39aB-d-Q(BMT-dD}#g{gp&ur@&tfA~BN>lGabD zhWwY!6KyH*CG|KEgdR=_J?!0<{=ahxpM7grNXmk- z4+LZT;Lsd5lD}7uYUfm=eR{8tu14ZR$A~TXIA`*4FPuv~XYj%1=>-~E-fgt}O-bYL zGR@>}GFc5b&HaR`u}Tt@cxow&Ek8qL$2R!*s!Q-QO#CdJj=#)!`)b^YxsQF%$t~GC z%NV9fh<(qoEt&D@fG<;NXtD1(ur2f9WWblJG*pvA<-k|wi5bkEuFUWIP^d|;BlA}} zz$>^ef=TAUAi((&Y{>kO27qJJvx^WBsvi%+0jb=^4M zO_1`P`EE*-l=r#*sVxL#G$y+#RsOUJlH(F-=H?=_v_+*!lYP&=Z5bOS!iY>ym@RDz)5(~* zNK|i==@i&Yw6;Br<$BU6H5y}%?+jzeE>6~Fe~wY&$y4)wgh{3Pn5r5+ynd-@PNVqU zgt`L=OKHlGhfBbM*UB9IgEk$ zn#q%!Csdx@>}kz-NAkQRMb!SADdATo{}|db?vtg*WSW#@=;2!ytm_vG8i!@8Wse;Vc%*I{{qh)l-(jUw8 zrzX~j1#8X{L8Dow@0nP?uwXqaOJmXm_H5`~F!qK8OP8fzlj%wm>#Z=BD@Iy+jZ6id zzlAZxd@AocG^PGiRSnNLBk{MBhy23ykbg=K*()ObpM*!yIZkxBz9?(`CZe?uWos1b zIo?t=_Rm-)o@i(7dlaoWY-|>z<#ic?=rQ8p3o{KLb=ZsnIh#AR!`6nD?R$0zjtCJx zO6NAwm3cK*P3knpvF+)~xH?_r?~th<=t3ovZ011edPkOCC0P&{Nns4xt@dE=LA}DJ z8myj>_-+UCW6-kbR#!-trP5{)OOx%*hSK)RT5m?QmMmK{l}6QAX$~cxXy^GGKqu9v z8m+#TBV^l0t)IErXgyW7et4_suxU2xuoRmze|9@C(``nN{lPAPxi%V~Fy?TVCo7B z7UYV$SXe4*^=!k=RcvS5o`!syqgP3nuM-h(ozVl7tp7#eRhtD#gVcAf79<;q32D_JXLSD(Wq+MQ^yv(U8-S0p0r?x?ZHdTX$CB4AZQX{LJNLb zQkp9fr3HU1voAL43kwblS9@LN=H`p$pGDikiha_GK+JeRmVPMHznEA73)ZRvLE|x* zPKNY?)~yz-@5|C-GF?hoJg3~wy0h=uixG6yGC}J>nbw=M?h4a#{aBXnlZF>`J|}J9 z&3vECy<1wyoiS~>AlfF=ubV{gwGe$zmNpqgd3y5IFoq2OWL%D9GnII9wyZ{K?VxZ; z!xe8T5={=1OQv3Cxa7fcE_qP;;FDW3c|GuKqz@j7^ug!G`QY=053n~)=w>1_sG)sWV*}5`lSWS<`y)T%Jln$#Xfk{ z;)9=)rEkmhHzut=g=x8F6bf3`7l~BRc{|bv|7!T4>xUA3u7S?p^?sP3^e(a@d)F-N z-{L;&T7}KZlMBPEPDmmeO^ojYmI!!QAx)+TBVy=eJB2&M8(OJNkwBM{m%SO4F0rcy zk&lYqz*Cg%MC_8w4PuutF>~vH3gBJzJA1k^zZ(F2xj|J-ROU&r!?jS-^vP71b&lPf zq$u$;jOXn{{8w}Bs=>pN5<&hL@$#U_ORnT)@3!o(QoFg_5Ut$y9dAWfHu_s4hC?sjbA1>r$zM7MTj&)kxhD63>B240hA0 zN<3*Q@1vEF>qfh3=yn{q zlCWS*x4IN(Q%4c=^54F(o_1#JagL;bC0Fmki$QtU$Spa6`}Z?NfdjmcJAvbJc= zZ*d`3165-+OjF{CcHZB~rEayWMytl(v~Hx<+paKLztvO&OS#36nRy{J@IpVsrpwhY zd3Z8{m#tRG$pi)J%LS--hn+)((XjEy$cKr6W$Ibt@3R8MC^BBb&@MummJA+wYv{Am zt

1TSK3;wkTQk)!0rT?=W39|gQ#~+Ezow;23^z~N#gwNp`Z7_zWqJt{z@J43z9@@#^g1ktWu`;6Ank( zhori;W0G-NmKI1#Pn%f#!dR~5vh*7=T~3b@)W_^%Pu|rcv%e-&(ad9E0 znF^c(798H-xN7z_pge~jolmw`w>BztUG*mt?FtGtlkE*g=Dr(|IbUSX^)(Wra#deF zGLuE-4F=|umm+h4$ZRw+A8J76l_Im%$n;esbD_xWFf#9b5SfcaW|xtj)bh-LH z)CN?Cp()<29uZK4zP0)5@iccDwXLdGTb_jT~Vvk=oW%-mc%>C^PlqpkI0tJu08S6d#zp<4naZL#sx~7@4Og2fkz^yYWFx49hs6?+xu2cG zZC)}{T@**$UFu+XP8wt+wGeHMIhpGa?XnIo%eDZQ1Bfq6%8r{0#m$?d;;|Lw2(7M) zBc`tiXW+3{nz|~^AWyb%$9|!RTTc!*8t+?)+MyV7WofQ6T-8A*iQFl9Y6y2znq zBvFZL3T!?d?4)GNoW*oQ{9G00hcHvqB)^N|%y#i&cbJlfZ^5KrU`3!@ zxM_NgB&rxj1Ag(R<|9a+&mVrL{xKMk;(`rbun@B2Pt-?8@%OhFs=;{yiW2#|F&q^D zOPL20*l-_cZS}R`umZ$z`gO7&w=s$W)pz#d7Ip>(e#$Q}u5J!?b_JGn_Fx*wB?eMg zFJXXQTd=2ve!r$0#HbBl;HGXm5CMe!o$UbSy^)Vrd;_9>Yg3@fsEYUvgCHL_8$0_0 zL4m@*edAxB`TCKAQKZe+6u>Y2iFc6VUyrp(L0TXk-6GI$!Y}Cj_@NdcVk8i3rh>`x zc1dowfVg#_Ndo$6y`{IOt&{iw@lE)7B(*9O)7gtt7`g!x!Oec%*WcgO>6hZ+EC`gK z({y+GTW|+WH2MAbr5;fxwFqAdlLu<+<{luPG3>=THe+696VrXO!M^$1k+9^CU`6q}l)l?)3&YxH|S*{-h( zzh=iha{b0Vs!9x@g6^i4{$6SeNPU40{6@XiAO-|+2!7W4P2U!t9L(M^)Kq7R&UPZZ^nxrpw_*fp~;n0Pk)KyqoUs*^Hhi=Ew_aJJFZi9P^auB7eR2fb^w5waoCL4N9>p2rCnQ$8vF3^So@fgwj;)7_r3Ri(AJ$4 zquOV$32sEGZ4Z4p2kCnmW3P$b&v~(L5ah~GwGFAelqy^ z!OtJGPfk1GJdyK^bH%~IoP$Io_F=Bo7W+0sku+8%Ma>iy1?o3}VRxp*+HO~;5vABQ zv44$HsdNUKc3$B;;oM_enB-g^1;sNX_r&}A+MVUj>!Oqv&9GmT=G^$mBab}l4DQ(I zT*3cVa+8M%pT6w2VRbsv80Q_a&Q;Dm&Tly%c?4Q~W$Sy+wL#l9(&Llrn&1wqAQUOS zKZgur{kwZ?DM=@ub?&gGTtYbGbb8GUXU8K^^4BFjw(o{LgU+8iR~p=**3{xk~qx}<|-aMfPsY;cy_mpkv+bMVg56YFzNM?o&0@&0|z&L{raJ)0SEGi=5xI-_qa=MyXgf!I=brW`WrZ`HE1rF10+I)F z;YF|B=G;wgbQ`(RQ}#7$p-bl@&T?C3G?iYTWOL0#t!Hj?9ye>fz_nIfs9r;o^BMG& zw{6Kuhsejt?OzFQ1f|`#IlpPT@!yHkD`>tVdh@MG&Zr*NI>UK!6zN-My+3HXa%S{8 z4KsqyrRY!5)K;HlpZeZD=h73-uS6l+JL3^lJ@M?LEJl#U_~ESqsK4f5D^6fT^t%<#V9qm9h^>vo<5=V6@&`l;liGU)!GJyn^XEx%=FKd%Nvw3ZC{@XAUKU*HLXX);527 ztn(G8ReB2gF%aV%$@*_M!%^obhANfgaEZ)se+x?WpXqSvjj_VCd`n9C}4-kPd) zAh|I`(~Wy=W2#nJUtXR<9M$TTRW+XK^1@<|mYWUMa0E|AX1?yJt}QEP4l_JUva(9b zm5O4$1czo2dEKiinCTYPm)4eDr{!l9WGZzv^&Tw)_3O(j>#{PL3y2r&!4$p+2Sw0N zv2-23Fw+a`sw&Eg^>xMG!Wz9!FRvr?o z0exdreIJarAIK}X{htmR1&Xb8yCLH%WCUVG=|xK5=8-I=6@1*~$<4^lhV@#SdRly4wB+dRSMZV>s0Z6Ss99Rt z;483MQ-Xe9D{{~VELdA#1lOo2EY~Z_$WznP(&>Ub6y%hY0Dldnz;6<~P)q zAqVR=9dm4)f6)#ICa=^3uFBMksuB+lQ-WHdXYvI8BqvvD$;o;^)AgnRRxiy#oB*Oj zi@Hv0HoE1CDezOhscTacR!p5eSl0Vc!@L<^H3AWxF-57UUCl>&=;)0bU4hi56wR7N zXS;E(((KF14D@!m2GCdZW-JW)^sGz`AljEsTU=FHTVFwr-bu`mh`xR}A287MiuJPE zDm^1TH#-;HXOgxG$`zeLNMSv^9z-g+>y%aLI8Q4;vagnRpwQNZ^ZWYywd-#L02`E% z?n}y66Rix{2k5+$h<@OA!R;sLA0Qp*&}qTtqOa8Rx(k{qGMdQ9p>Ux01p_U5um_HZ z^K4u={3TUy!%0{!Dl77kbpS3|N#G_#KcC(g=+{=R0K&L@xO%FVo}#VNbiEhxs;#Sc z6Jw=nE;B07@|cLXbflzc`0eTVg2m^NMRQkOrBQoShfG6VqpH->U3D#A(J5Brz{G$q z7SYuID_vNrwTiHQUU{+CQ@mCnfMH887doQ;mXWS|8meK9taLP>i@gbJ@F1mZY{D8J zCjjX>Hf>rA5a^{Pp7J`1MATz)vw?tfczP)0qE@-5v`)j%Bk10bV`+3~j{&czK}*j_ zPmgZmVDtGQ5PWsFoE*7$fqHAwmuidevbx$7#d=f^ zH?+F4zF4mCH6hIAvQo^Uku8%>ub4c zEus&N(dE?b#SoH_mXTkOmz9xSkdu{@mzkB3mz$HG>ANbsAS)BGONpTsxKIS0xwMMRj(4zM>1zI{#CD_y48^jQcfjrnlhZgq80WTb`nsEvjFvH%^gM$xg zP=Thb*5I4UT8O;9vRJ2qxv<8g7gm<&wd)G2^$b!jc|FF*L0RpX*Lbd+uh=CP9*Yzg%CLpp(lrlR_e zR-horwQPXgGzMTUsbg9y?xl0*XJ_Z;WoM`7W#y$8rd%H0)?Pg`Hpz&9Qi1 zqU)_qt*!l5OIc1bL+nv13d_oisv7jl!V2nTm;q*B@qi%$+vX%V1ymj&c{a|DiTI2z zV(sKGs+dF2P}6|fc40Zq-!qg_c&(?7$x^5_0MP)?6D{)qF$v(n$-_VI8EXqQ;s%H4 zp|YnkMZ01JMtp@-IL?tMi#;hLibcqkifT*r>bjbeveHs$R#TuvtymsCVa~n^i?7jZ zJmq+vXpWQIo!6C>%1CQO1t>n8NuIo}u#CE8on~O5OMQZF0wNVvI}zaG7EC*QzD#$?K}}35m~rf z2tveRl+J+gBvw{fN)#6$!tpYzv<#*~+(Cz>Zj9cc*H+cnV9m~50kNirR^wz?9Ab@U zJzc@>9SXfK^#mtCO-xndt+xgac=A6buPMysXT;+&psx!BODo z&wk*Xw{8#bDKG)HeAGE_#I8tn6&iyvt-B%!C|w&`Xt@}sDOP-#w`>USh+s5vQBK5; z2sciw^S+H94r|d5$izrc3;ByVT$@8&eRznAw$!ACqpU4y)?qPc8n%hj3o`RD4yWhk zXJqEk`q;N5PfR?_F2=nmGb1}MJ3lKon@$;0YCODkrIl34JuIEq8&>1B`7i@?Aqt$s~?nWqjzF)f)g zaNOyDt0}da!m$DqlpY4Xu#>7&N}Q%0_ISLP38THZw?WM+yH`owmahrMYB{6l@pKx}FAZ){0zXSOb#j1!66Xhv)+=C3-U*1z#I| zw*Y3T#<)nk(k|LvOzrpe`2yII$08y{yOpzW0JNEh{V1{X%{S>=z!3R9xtk2Tyme&V zrKai9xL_QfDq}j17q`Mhq|a8=V-gOh&4yOFf32^rC@ikQY?D{tm@#)Z^>6U?OP4mz zBVJcoGhQ?UWEq(LW#zCrRdm}Wi5*_zf`_MLw_IwilaY0LVrlZ*E&Cy zCtIcUmBn><*pM>rcxFDanJ1+A){&)*)@ZtymQu7CMekKm-^M+Si;GiS3+X;n&k$v_ z!)mdsbV7L1`Fk8NCeODnG>HZdX3V_bo`H!34M#=gYbPF#D8dvK7Oxe<5-(A zU2APKw&h`$26R6TRJAbM_%6?6A0vUGPy5Lj zdT5W24&dfDr?6iH4ta@hZr)+FL6MT?-taowv8b=aQk2@#DP7zSz+A z6ze%T1w7`Nj?Pa;L{|xq0DX9+3TP24ULF)g0l5kM#*E!&7`JR}Q@7y#>}q;?(%RXt z&0mU}`4EqvjnLK@*2_$&&DY!ZN!O?7;MVo2W$uLc-&)5%R6<@VG9zYD;SEkP;{y-8 zbuONaV0*GRh-XqMnQ57r*5qa7=j0>FOwY*5&q^=A?n*lTei5pK_g&?#D>M?MJwFY` z;v1Mwq!Gu>fyS86n9qhhS^3!|CBUL#q@t|0 z7~U!lFUNYc)i;0=@$jjc_S$$AOWO!|1jK(?LwJnbLo#>4T}!g^Qp}mKx$#SrVRA+= zWO;y5!1H(nw5l3RqOfPsKzAIq#gid2Dm{xV#;{-K(X!}?;(EOp!N0P;TJv@JecG+s z7ER3jux6wgJNoyMmEmVucq)*-95@o0CNp|B6=Q*o{UkijSQyU3?)CDIqn1I`qPIwN z(O#IIuZPGHV>nm72Y+~Ag@)>#ZJGll?Tr;h846aVB~Q z#VU50^QYOyt_2OFw1tD3#{7=NEcaZCc+Fef)Qn()5F4*3x@fg|klsSclS3GWYiOeM{Z)#4}GI%ULf4sErP{JmCt@@Ty`w z^P))-hb6J!0Rz*+S%m1y+ET28OR)u7Uqh2xV}LW`PZqgNbw!~;eHHSjXd~<-v zPdu<+WL8J`N=N*nUW9C#LmMHyyhWQ2vy#R9F+aJ+i!Z6kf)%8W?c+COR zgi>s3@$yGLM6UH*qZgy=<(#(#!K+wvh^r}E?IjJ-NbZ-ri(yfnB)55lyTVjOC5oJjFt4#a!RU;p37mOutF2h&y7b?V#UHUYx+A(^wgdn z(YJAc(q;{sA)Yd8RKmk z-u$8+8LWZIz)YR1tu?i+6~2I11kgogu149K%tzB=ac(TLGib*URK>y$?MDf%DCSu+ zJ^LgTkz6#2_v7Vno!*fMgJHkG%hY&X-r^RfGl&vAi-8q8yBI@bw*Xo0H8fO(pKkIp zzp%Et25gk#nREcZ1=wIbNn}$+YMu9NOA1R$=zS*YkzmiV9EYN;Mx!|x`W%|Bt|?qy zQAoS$;*}*VCwR9UgB)H9;RqbiWGY?Hm}a?*8_Wqw%!t?0@MjHMe7rTyYiF7lviVr; ztk)<3A%*M;TV41OXC{xpBGO0(QHiV>WmPX0^Q#*g^unSt^O-RsY$k`;!ph33I*$u~ z_>11(f*=%)=yij#T2EzRQMsptq@*_n@Tft&aR)Cu59wO*NL9RPAn;RC@hC#p0DJT( zsBAUfUjRkpVKR0sEH57LwuVu(5W_%T8*O1=>b7zvf75d<(`Q9T)m+>ipfrSMOq=me zhe*&OE68{tME0Rq{^^|q4qR=iovA$>Fh%I<pJmP3KG6+w|F7X{Xx9MOR%dYVB76A#42OE_)af$*!9Q3qD` zUjz^!3VR!?;_(kBFm}`K4K40?=;lC;zunc%!#X`8rPU(2^tu}CL1INqHsrCGhMVx_ zbi@iS9S@DuvkS12%gVsYEj>TSw~#h1hSQNURPU7VBB+aUS;F&WZ_pnn`o5Q zfC6MZG>}_*=G%?B-qqFGxzQ5wGvrUcd;^_SN4yKz*)E2B+B6|O(Y(CGLoWl0aR+Lb zs~iO7cG`r1<0JCwXjr^1Mty>}9eAstqzZE(4`x~j9>$ZIaM+f;0`EPw`8YIVAV&up z2z>Iv9j}z}$i0fbx$Y+&+Obz}Rxx@GlZu=u7&!ko8`3D;vclW>$zFCIPB*y241400H$+X#6B?FjI)))^H!PsMHF0$xZqFoQ$`BWS}mgV>ex8*^MD2JfwC0v{|#12h9P8xwZRV3!%6vO&`dMGIpyylk31ePDj(7ul3RV+1>>c3@l#TC3P13_(Nz zP)uO>Y>Xx@@@k<^jV74A(7Z}=4IC>|qH~|ZzuHpx1>4|+#2W^?rOEVm*_GwEx~1G# zy32_o$(w6d2pJk=S$k|KS9K>qh~YDQwOJ)p4K??`m!k2)Y8(ez06Ctk11@qrC8_C$ zDK1Ef9!PBDKyIyFfD)ClIUj5R%?64X=UFO>ipp6=!b7Ugr`zS?2nJ;X)oEldc6o(* zHWy<8x3j%TTdWMoyfo7QpogFtS$E2F)+>)?(as zCEvB+U|>kElf}P=>dQm~MFuK@AwB?t1#%)hrI}0EXl;~Pk*}huY;)`O=Kk&7tvy}B z62jQw2=L#f22nHA{SINM~6V1V)x0uRUln;s_J5#ZNvwcvK-r)M;hT=^tPVquzaT9a7 z$u9FTTN(l!z=4@LGt^@q;}wMoH{0VgYhHG+d}M2Bg{ES*^#9gP)C*+KV`HL}(hScC zgS2CyZ+oKhpyB~R&6L(L>_yqXxEjeZOPOZtEijFlM6F>-^XgUHrv>C@u`D3LKy#M# zK2|N@wyfg`JkEB_&9vgK?zq{qNp{V3)%#YL2OFD>?HHsWHST)m?&xHn=YmNCq*D4L zE819dXz9&tjsy>gd9GQ#hW#yaZZtZqjTEnmm~c8yBW4@B88BqA=hj(7U6q1qr3aoQ znsy0;R1#`MbR>wW$!0a{SwYhc6b7FPNb7MXE?PFis@(24S9!(tUa&1#oXqtO!3vynQf$V;*ck-WS2P|+i17K{9k>yg7vd-Z7pVAZ zApO(Ox7bWVi{&_vVb$cSzA8nOqCzT58ATM=5K74z)7XYlqf36Y87wP;$dPN5=5C3; zhv*-xmIaXm?jCm+F>;b(GyiLI^}?wrV15jNxbRp8HGb(v5^)p>w9)tj1Px?wFgT-? zfRHq~l7iJAj0OP{%YpeZ@ON?5kF9L>3@@unN?u7yW<9@WyV+#g0R@Hc81; z?Jlbo#XUlJZ|M0&Atr7{+B*E4b`u~!&`Dib-99T+VOA>k%#(n?_ngQ4n!rd$3h zR>@kSR7$k`PN|oWza%Q~sJ`s;6!%sr0n(0?(oj7u!9r4NsIeCV*1?qj(~h{l0vtDG zfFK&?S_TGH{wAoByOvSdh+&Vx2ZXPfH@Qn zhoIwBUxSk&cT1`Zw*qXZ(FIyE>8LMcNQLNA$EQ@0D zcJv1H^O-vdYtH}lYNKWrvTS|Qk}7b)Y6_bxYieopfSzarPYZl?uE&}Qhvivu2SD+F zE|Iyg);5HQv?DBVCORj8PWvMXPMHv&gV>jgwb8duop z*aSB~F^J54w7!x6tf1XJP%)+m3$2RD-CwqRj%o`L-Iw5_rB^xJxT75ssg2?b%Jzxd zBC~1rWIQkrWnK~3$V!-`YZa3!$A_@xRebS0JOQ~ec1w5?!`6V!1_Jk#<(PMiGdm?o zxCP85x!ml#sWm7~27ZPSIe57=w?ax#CMLLN8dRx;p?c6UQk4v{Ik_*_yM`FIW@=_f zQ_BV#yuO~zanQhGR#gbYuM}pLihO~_3KmmEiGaGx&u^*&<>VzKm#E)LPP8aAaaDGp z6u+zj^2n9Y=D~E*8ZRwQn9m`_BI5&O2uN57wWfjQ5^!ly3I}XOiiu>iQJg=Ih|{`V%-X~2-ik;A?)vs(;nA1boFxXTQJGE zM0eIemkru0s=c5f0M+Cn_zkhN8DN09FFRdrB}N9EUn-B*f%CD=|5FwNGhnxeDuB@R znGJxp06P>M7lvQdhJdq_+b~egB=3MLpJEhxvl+l#9P4243Q;%I!UPjxDcXdQ$c+~f z^Z2IfCUxbrnpEbJsIRAKs!Ve|J4&<;w=%-oE~7e;UoE~#lQS}bnN5*zDVBNG^GZV1 zF>G&xs$;b70sn7nOTQTBxBGQ(fGtM+Q| z{}RY3m$Eg)5TLZ!zyH$1Qn$7yiP3IATePV(p)|af!mIXA$*ARwrHqw4&m?Bz1R>th zqoj^Ym#=|rg{A=<1!!W%+=bqy6^ZLNUK3LV$b zKAmRFtMJ9S8)MuEG6H_hZdngAiD8&nc-vM7)F|ROY(a(9svUz?4sA2noVmVjkD#}{XyISLT0E!Tu+brpk zdTJtbpN>|fnha?}(f_NhuZGbdpoVRznjoe<%*0M zm6A821|yKCs#?sJuw*Im_E0XARKO6?ULOK*R7U1O*W^G(hcFLSFN(2aM`yfC+*v4w z2l&0<4?r0%Pj1B6p~jA8hTH%)iva|ay_s<;zQ)B%un61z4dJXl<@a%FAxN_T$|*p0e$Yto)JA0A@B zF%#QppL9m^4?WLN+@SS!iZ(JTMEVr_%euyxh`NmsQ57rgz+cC`s``WQO%4rvj^)H^qa!I1Wo zC0=|wsJE9eI}7Y{r)O=33E>?VOIDV{NYtTxdtkNoR)l9zz^(~T8ICb+ngt6Xdj80U zV2L_6koDxk#aeDRdccMF^yl-SKgvBxH}@(jGZ^e*E;b6bWdPBzj%dGOWS7AOrwcCSxlbf z4t9?-e8}MI`kb8kmdnfv;G1x?Fnnl|#htpy%pre<_a`Vx@rB$+8pIHpn16yynjuLA z(U%3aFtBv4Xd;6J+!#e8L8Rgu0DFGBu-qhqxdFp$klKlq)=S{v?%5)8S}gM|-QZ9r z)8{$|rV^cpa|{`Y+&{Tm$XNZgS3KNR!gMaoxX|)0XysDPhWsE|ibMuNcTm(#@1VcD z{>?eD0{Xjv5?@YiI;vv4MDdMEb0ua~)j|Oc=0}Z(+4;Fyt2V`BwcXGx z>4)#Bc&rL2yHx5G%ibOzh_!5lyNH}D7DxJl#I>J;8=NX-cBf>~nBKzD9Z#ZnRJ)63 zFPUtqNP>^0E{eCgfi@gnP=O|DZdMxr@1END_;YZtF2W!!$~QtnGL3|eg20FxFRn&T zl^`^<6{uf@7sGzSs;Q{Mb_GdBB#-BT1m{Rgzzd0ynxk zT9EE@hoHa$i1Uq5If(apE37Q_pxL;upivq6ROt|S zw5Ev3S|DxcCBF}Sj;up6`>B_?_qk7G23K!DyJE?be6i`L=4WAZpS7?ri}@fP!v#R9 zP|Tst;If^rFv|7$;Q5TG!%|11sdl%}(a7Z8fkCc8#O+jyAQ-Ln6-#R2{a{DKNBanq%M(qs^*No{+m_ zRxNJnKvttZiH48jAc!9T`O#98g@X0mZ~**~6^!0=VEMt9S@dn{xisZ%LVzIfatfvv zc}LLuT<7Co8|I<6@T>Qw9Vxvn?Id0hky=4SE+8T*)FGlJqTxt-3xJybjN={e^+Ekc z5M{u3H3f<03s-e*Lxf_LVuqjaC@O=?4>S|^r?QfH{8+PUEw0Xn47?AHGlYgStPQ|$ zb_WP5-h>u7Z<}45+Jy-+iKHicrkNC1yLzjlIPUXW$lQkNRt*Eby*f6gR|z zOKBH)B896cX&lrE)dr0RY~fXi@8NW61Y~|@eofu-3NUTxSWY=POTSoZGgZ+*b4^kT z^5CJd6tqcEaak!Gbe7D`FDodC&oWL0IFF}srz5>&9GV~4nAHr~;4;Wg8tjW%#(}TU zrQqyQd(`F3VaH-jla0l4BV0~s7#J2oJ7uNDfM&(`Yl8c|m9RtClL1N%nmlf4Z3c4$ z3g04!k?zCZLx@kme5Bb^Uh+nj%R$ks2(83G#DicJyxherE8t>4CMGO~K36(sgvzw) zb0X~5_VPLO4`BPVsWuJYHn-g{;v`?nN_Iw z>gtB-Mv>nIG@8W+n_s;es|&hDZILXQzwzlS{2%HwQd|jf8GMSabiJP_{vvfcs;ZS$ z64)H#Pa&lpLJITOBs&DE+(LDf`wpOlOlB??DZ6sDAgL)rF`+SFl}O19Eg2k2j=~o9 zY2G%A`LxvzpIO2UCH60c6Gd;v!h|L4mB3=9t?2p?S78$gnUmR*oh;3jn!+`4x9!^dhO$B%!eh zveB63yHsSFDaa@gYTs*LU_0bGkw9&|J&{XSxwol8{@>pyQEw^bMhUtzTVvD8a%0oC z9$>G;eN$Uo7P($#%T%>&aUt2{OWmc8Qw{AY8-R5=v8mgXZw~kiUf!^-etA=)=c0qk z+CEmjFt>e6m$FnzV6}q?hL;p*13=6MOhW<2JtrCcQkqhI5wDy^g*BKfrgC6EL06tJ z<)jlO86+~!z~=#pFkM64iC)V?Xg9oM&Sat0j z$S6WYXjDcK?~1_tb*UBW(Ki^~m;gEJVCN#6-IN2K3`GpLn5;;i_Z6}{z1bx;)4On8 zwTN>V{h*|~RFU?c&XqtJ7-6enH{9vf|R>qQc^`g1Pzd#a$SmU0gz6o8GnsIgQph z2SAXNhbvq&9}-tYu-Y1DBlL@{rLxWN3^K4a^*Qu_9E^TKT#p{2n5{wd2tmbKvHE3O z8!r}~jy_?^>@THqevJ2B)qL#)TgI?rX92&c&sYtGLA4s_zH$w$e74n!L_#e-N1Cm4 zlGsI5I2EK+3QuTHiba*tyO4yMR|1LKn#DqCL#4xK#*4hEnf<|I2W3<%*Dq*W<)Xm# z|DyCdQuuvA)_~KOe9j_4-p;sqqvKKswn_drk>3i(Ld4`eR*5pdbhcrh zJj`83lBiWKUQ!t8?nIel3};S(0;1T^wMz2}1=P=@#70znY&CGF*+`AR!eX46kzEFb z5Tk$NPETg`Q2S=g6T%yGr82-jwG{X{uQHpkb!*+dPjhxlX>o2#X%YSk@mGMq{M?q3 zdH5^C-(38a;;#gM$X9}VCCFETd?mnxACX0XE#sR z3+lDf_7b?=Ax-Nk(osSd)9BdW-Pv71&6lfIMcl#*m6a*qj229I z8sucJDICrzpx*>3WOlOFlYv55?WzxBgF^-wxuaiLY9`WPh$P%;$2cSLWFi<}vcZ(i zKlL(|yh!Z<6NXPpqfpO=21`69a?cL}79vnBRQAP7jM``V;z9g~3a%2TlNJhUtTs^txJ>??&?E8EBzc(rNIf51(pV&+qy zPQ{#712pLVG*=vQ*eR zP^#P@{k06|cG18j7_&TWWW{kNM_)syyrV$NX##l4!|U zgo7iF#Ss$6$N>_9o|qZnqeS^(UcORW9;iaqj=#FDhMR0T2Te?VP)##4VYR~%W#9rISqrPw1$_D8Rtqi!Or;mIErJ>uh%KHlXds?y8H*@DUNGxC zCIGA=dvi|6KS_#&?mbReBr71{GE6y)1 zDJ?E3!`YC91J?7#}l=^zL zr-rr_ky{-;ci?$Y1Xw}DM`aT9TDADtJJ`xE23GhgW<;*53_o_#b%tP%bR+D{3WZ|Q zdLi1FQW1hsC=>;4R$k2Sq5SYUN0!1gDaDDUf-VrnnC%&ta3xt1?KM|aOCdmt?X=Nq5rrpH5elkyHzr1l2-LC%@-sM|z~?qtn%G)6}^ zm7Nt?8`z{_W&xHf4R?@nRDaZ&A$!h^;nXx?nUIiMQMtUTnl73-Z%M=+#H6Dfptw3& z922M>6|#)okYHXFj__OZIhr5s@z%j4cccLiDWqkI3St?KG39!{L(5=X$^j>fAx(n{ zGTgE&tirBA9JiAZAPF+YIB|SYZE}whjB&@o98g!$WP_#7fpU47q-~UT4L13%*aFNE zyxh}eO;Eqc#(08aIwbHg&A@YFYN}k$(3h-{t9OF5rH>+*%E2iBL}f-J_VgTrq|>;$ z5WN!`wFM2qAp7zu<;kW}%&%NRQu{p-4S&`AdJh5f^x!GCvH|lkJ?Pj4;#rI>Wd%+C zmEv1M+Y;WNvD2mwtGmBWxEIUj?piqt$MlLrMnp?j$>&7YN&N;+rrzF3X-mhl^^l0&4=3&n;yh3)9sH8p^wGiYw)FWU%M#cbZsw9NeA}1UUvUmf> z#P$!uTa{R*2|#T{sT{8ue5oY%$}PS2-yHDLk|1vnxPtSE;YCXx`=1IC<`Yq-_s3{; z$Fs$ZS2&l!iORcaWhYl75;A4AXC!76Xr+(<0EdJaqFLb=awbem^`u2ZdP!S@`Wf*- zPBCAEV{D+fV7MD89#MNFSMgJwMo66u9_&Vw9q&v`kHcfcYPhYRRLY+;$KgQMOu3%k zAWsfcTncs^a(Uc1&WnvpaU_H4ZtVhj2+HBu5i1L0s@r_4V{{z45G_^ogpejubPu)OzkRTYT&~J@v*w;ZUPgzK4u>&e3#k0wWZ9 zH=!*G2CaB^#mJS6w8|p#(C4}EW!1Fqt66&-qmyDd9OR8RcvZ%lhDFVPn>CcPlfW)q zhBJ>8&jutHYUDEG(N=5@aY;*twxS1UxtNR73~{cQGTI=(IDZudX%8Ut6HxFIpdE`Le0-H3?Ct#V*8&eX$NATlp<=wTNX zSTht1U53HMMNa9pRL`DQ!t-L2G@$5|P*mQsF`ZYef*KZLqcJ5TS&On_E)^@(C;MJh z0~Zw-_+8Zv!&3=H`uEovq>-2qq(&mSdk#ONCD_eMA zA#%x4Sc$gqL{RtqFj*~N0RoJNH3`L%z)1H*HtMWR0m@NDP91$F)@hvX61C>qS_U_6 zqPemEn6{M9lOQp=axgyl@1NdwItofv73G!J_ZBJzo-UqyWBeLElTw;Zbwu?Y*s^ky zA@&JMMxD?`xkeivXkNMWK!v*Q&vL-;C#9vFI19R~xz6%WGb91E3n8A015e>8=b=>D zIQBuHHdfYxHw)c1m_G?OjzD2AB7~1o*hJx{vCu<$W70aWm{_bQne+?o5~!L1|Dl!$ zZZbIPM9PkBBp$^~QD`eDlkun^5Cyo8LXD7Jt#c^_4KiKRT@12=pzBf|oGstsiYTUP zg+53gne;Fcdo$PFJ2WxOeDpcKOtdQ#&!M1JCDfKFx)kqNg$9yx#%?8WSB^8TU5xW# z=c_5*Xe*_Dct_0C(4AVn8B?EhqclsWxCI#xEIEG5LZXzQGPY&LxK0aF0DX(h%Se_Jy(@BaSsdB*AxL(Z(MK@NjT>gbb>nQmiz7W zCHYmjc~%Qab>(cufA}3nfs%m>Vxlw*Fm3l1*uA9Nxp3Fw4HWe+RwZWxF(5UAOKA$i-7!!1 zHTY`u2e;+MwxhX;d43xopOb9a-z1wByH990C7z`Z$B<`R4C7iG-YLA9TwGTwLwpx3|Y}eQp~M z$Ku{s6hmBRdM@iwGfk@2HGtygCX1duw!i@kW!|4J@>Y~_z^XgOQ@Dtm@KjKJoEWm; zMA-OdYF;#phXLZd@)D+xOC~G8uVf+`H=YF~?z;3h#iL}OiF;SBDl6-1>q+k_B>?1f zZQ-Ta^>$Hc?NloihvynhkhQCXiG`t+s~K5HDpn-9=Y%mU`&aFph1Ec*8qRJ?kg6e* z;XIgQ$Jochqg1D2WNXG64`ZZ!ndd9U{A7dJP5QZSN)e9-UHcx5nP*Wq<=cmRt9&_R zSTvUP#!~jcP$vRXvhDE|%hNQO(AnB&vYaM^Y?wu97`<(dX%7JWZ+~&95IG+xB$4v{K+nCrmU{Rpss|Z zlZgb2tTvBuX9|MUKxChAq&C16Qxcbh_>xi~PEG&PNxl!w%P%V~gdM?LDBqWq;Bd1d z=;Px=GaMyO3`$zZxi>OrGV5tXktZJYqGn0KJxrc1gS-^pysW_VA|J786?S9FN`XUI zsrIj0+SG8ISW~FBmYuQdDJO+%WNrNp3%EhGaZRBfVOARM&7r?dYk6r6ZrBX%T7dH~ z#ik-)1d5!nzr=zBjUJ$nY{2v$OsyAYDrj`M4SYl?_hHZNOY`V{hor5bbnlRB0EObfDKErTciL>;;(`;BJnCdG0 z%keha?bFsioD|{fR8=E8fEICeHTTRMznIPZNDx;p{)yQ2% zESoIQRJXP7yp*C?E%HjbM`5YlL!miVkGRyMWRi9}YSUE&gPp>%!lL3*43(0?va*tS zWd(&WI4=XUL+Q+diKeFp@vNS>D@mdK=kq<8$Hi54qf4o~N9n^)HPiR3k`&04J3@A*=#GM$dBg|G-F=r+$DJf?c0Jg($(B z&;bl&@eC>fQkNs09jxY7#dBA5gx^T4C=c33bnH}AP*zr0JQpW$7M2uIKewcy&MdHs zkAlUCUJ&V2Aijm1I&~3~E9s5E{#As0g5NAT5*Hu@4PvSt zg4!T#gGFDAD+{#Fz|{4u#1uP#3-|$y#ddP?@>z>%`cLx%G0%7$L0x{LA|BqEsEFqt z)a0kYg*_wwb5JUehDlyUu!xwIh5ejD8Phkg673{X96XrHY{DBIBm7XgpZKK?I*K7<*rP@aq}h*5nKo~(I+13qzqNA+gPC@m@| zsd5nJ65}9)r0n{O9I2U7f(>=iB=g|}DqCnL&^tIW(Kml#7a->ot0g;EE7;|VTQ#kT zCmUh4q6chK^dsmX z^17z_2DK8wgcl9BqOPftfAA=xtsXUhkhHx{TIOf#M9A7Y%%n3sSk$B^xv-(ANl$iR zTZieS8<~4CUmla5>cOHWeXf3a$Qp{8^m#5UxqNf)OTIiNeSrsyn)Ed;Y$$5dUv**0 z<(qrg`tq3c4IV6N(%*7nLs65y+l3{UZ|>dW%VW~t@nBJtJ~E^ljqPL7V_jHs`R3j@ zUmla5;K8CMz0`#bMNPWag(a77?k)4>G3j~_7B%TJT-Z?5q|bC=$>p1SyL@>}`Wz1y zHR(?@qOyHV`coH{T)w&YZ(kmhwjI;fTcajzWg6H})TC_}mR!Dj&zC2p(~bv=n)Hh< zY$$5dFS)Sf^3A=MeR)j!RSy<5={=*o`kVCmE-blxbMFFQ9+SSvgGEhx!5FW6lV0e; zlFK*u7Wwj+bcF|tn)EMS*ih7@Uw2{2<(qqN`0|+an;tA`(#MST>TlBXU08DY=H3Ed z9+N)SgGEjHX%{vWHR)$uSaSL1-m|_uCjGnzi<HAz*a{1=o{k}XV{g4NX zn)HN;Uil_H(S;?KZ|+U<6IQVYSK@;F!ZlZKjXrZ%QyF)_2n_?=RH`|q~Dn7)!(Fl<-(H7 zH}`(+%VW}Sd$6cU-#g1I-=x3e!jj83_wMuMG3f_ASk$BkW_#tE^q>n%F5lc6^5rq< z?H(*@(ii4=<(u?g7nWSUxp$E-k4f+IU{RAkWR6$9Nsn}4$>p1SqkMTx`Y;a`HR(HC z*ih7@zv04?%QyG#^yM+>Z+Wn&N#F0nhN33@fD215-`so9m&c?Z_Fz$yzPre4ACtbv zg(a7tVaXyMxdZEO*s{aJhB-$KbRs?B@W_bah#wCf5m|q*Wo1Nq5r%&o8XdWXiFZR| zB7Yb`_{R*xyTeC@Gc+iC(AdbFLjcXlh`j<;q+R*wSsILDb(vkHmW_{eSoMuj8SAkJ{2!!UP+k2oswU0z0BmGJf` zU?rK65r+~sLBfv?1MEh7LZtj~0yiNH|0Hu_Mn?Fcs1q4hhRcH{Im2H*1BnrnBNsDQ z_>hn@V)QaVMjjL?KLYXe%*YDF8Q~e>$hAyFE*Z_sXv`V@!D3`Mb#&hU*V;C@ErdaQckwTC!kJNF0oDcI}=Cg2FVCd9ufI2 z@?=DwmGBo54jjqC51SGmHW^jVa)z(H3=fT%8o2;B*uMKE!%g-yXUqrekc`O7yz{y} z-5J?&9RSWXp^O_@>~Jhw8R5}0B5@?bQ}mLa;xXjCsH1jgj z!!Z17yCCwET>l1P_~KBZGkSU@Qf_f!EU6h8&P(B?#EZX#iz1bPgvXhhH1d9=O~OHj z;gQA8@Zu@RGcqe9JgUSwxK9wVG#sAmjQvwRZX8t>xkj?OIDI!Soyc#oeq=Z|**mtg zpy-qgr?jq>$-`W1IbxnOe0w!vqmOZhpIXlMn41~laq}bFvB}E_k6#eESQ1AqbcRhm zo1h7coP+nslM|11hMz3xIJw*z{@&sCl5?n?2OoUEJ0b7kqPK9VE)0QoJj3L zyy~DT=b)o@^XBksXV`)h0Xn!QvRdateb2LBUy0k14)*kqLQ9-shqF(IPsxaERk?~@sw*j-r+d-0i$eH^Oc*tcK?a_pm}oWo9KdJ5j<*tY|dP#SRCv1bEs9Q!eBJRCbZ zo#EQ^7=Ap5;cqWu_|RDlx1wPjdosG%u`9Y5lAL$!4?y%g_WUM>t!Pol{tV;Lu{(z` zd}trTZF2YP0(l#V=-6|lw9H!dndfu@&$ahu9cU}4wLiR~* ze~yL3v1b%8{QfkC+3Oh=&S3ZkW;nC^SQn4UVw@Ct!^^9H7`ksf(bYWpoIZOtOW`=tD}n1~%a zPulI|8m9ja^%559RN@BX8a;m@Zr zd{kQdDtY5a(vq*sDEs*pygPUu!yTI#jxS;u!$RuVKij}?s^G(zHm36~VE9k@x(fum zjtCQSau>sA1Vavzaj{Fj{b{NB@1<7x^O$GdLWVC%f4v}IeV>fYy9Fl?wR!gy!GU3d zCof5Vt+|TupGeNx(!x=}@T;WG&k9~0F_w8AIhkRG^x8Ah+FPW|X2Il#cJl6p(j#}S zVERu2-+dU`9oWbxMspnJDqx8&{ zuK;&5TgRh)Gux)14>H@2#P?*zAI4b9?D%sp!i`6u|1vkNN9$yE{%H=vQ&!JJxcR~+ zgk2rH+dUsWm${|08evc2wFrA}V#%i#qZKmy>J}mF9|pY79H?4~aIg>GkU2EsYJ^)K zVL98*WSQF!B3_;`HXq^H_V@YGd+irTBYMF8YyqMN?GO49{ltErP4|j@El19)_DxF= zy>9Q|_r7WWC-42%zL#U@_x2rZ-ap#En2+-RWb;#wE7B!Cq2tbo_rq> zv+uP^g#DxOxz50ICm*Jj_$W}PDS*P{r)&a-?g{m8=Rlo`@V$eRr^>r z%Ukvpzz*ka`yYJIAMBaztH0al@e6l_%FjY{erPVy|B}!hdl6j|n!@(FA#@vX%eg1? zKrW(tL!;PwKM3vHhv<>e&-ocIhVEcnz8!i3V@nz_V}2h1&dWpk`qR*;G64P^YGT8E z7J73TqFvzz7IIejLbl*J;jOz6?G8VOD=B1nj5R&Dfh{uPB!0>vh3tuumo7m#YA(>( ziJr+?9r}CX*kNa`MR@qG#R!i$wg}`XbnN?$*059bK| zp8X{I_WSlkNT1Qn?n&j zX&=k0r|dKMZBN^)Hz0b({(xmZYv09h`Ki4O9iI8V{p$imUk?A3U2s{LTZI7{uwm->EJM9q8cspL? zTX&9TElhjJ_P<%u|_j*3V-IbN|6%F?&BTG4BG_c+R1RBg}t^_*W1k zrWMX%>l9tljTV z{Uy_FJ~`w0xd`W-)P_c!{|vvi@&u-*0a|BMl0CZeJX~7^P&k ze2Cg*o)wYk?8uL^beW@nRg5xYx8mBF@;2+3_3hCJr@qP_nU;h3$eDhX)bjiDkv_Vb z2zbmN*pG{zVT&HyycS{ke)e_6Bj+Goyan%as%~d5SI=QT*4%O)* z;EHqH(HjxgpPGrV;hX&0E)G7uKekEwTLX8n{?z|om_Ki`=-_b<5Plr``x>K@sKaMc91 z-v z&t9_?(U`#j>vQ}#Tz_OterHz0c6US=cuiR}=nUbYAKBYMLg#?s%he~3PlF(RBV zC+pQq^#@FTv<4Ys7o(~5c$zbf)yj_&9||UL$twEFAi|Q%75bd=KXCu1E{uhz*%l51-h%UDG9)f6}y@$~y z_J0t$F13G%2QqK8m!T?pVs-X}M#pgP{Lp*skqbg^u#^i!-)3$1hC-~|MWL(N-Cqvf zQHto|(5;O2g?_<_|B}$@_(tc_&>r^EWuYFxb>k*##3CCQ^ z*X^&x_4;E@LU=+a@$1BMV+ijFRkQyd2wikFq9;RVwIO;bbnQe$zYG27Mnr!My~wfu zQK+XC(LX{HE<|)e`0!#xw}%TF5Iqo{ix)eOhTp>LoF~HT*fvjwyV*%khp!lm=(+G8 zh&?ZbZ#^8*YvB(tg9u(vYvLH3@sHgIvtMk|&~ZJ)nFK;Gh_hc5hi#UcEV{R+|d`}XGZ^!rCNvhR+V%`O;yJExd2GcQAU)Rl`7PRu_D zVaZc$mnDVx%FJa)k3o3c$QcOh?&qw1mVG2UYPUU~)6r%24s?Kg@B|@kCY2E3CL03B z8NZjUbky<3BAj$G@ZXty1Jf~!EjwlJ$q1(oCnimwPRNXLz~9nQQ9cCFB59q~9(EcP!B-znCq z2(!8;=zBBYBTD5pa?H*7)hLAd&vCF7Tx=sOS&fgD`b@q`YSP*QXxX-F5LVyBMvlL- z6Jc-TDxI(VA~cy(@gDJE@tlPSD{Bd<9y1SN&GEemmmC7bca|Q?vAyhy8idC^(~hw2 zGj>D$B7Bv+vpsJnuH)}dM%eL(eF!(c&sN#=j|+5;qSw#Hb?q_4@1_UYCaZ5NN4Vzc zH3--Kk+aIW6F3alKZ#N7ocI6-NzWp5uCwC`s2um+bKzBNy85ov+_8 z_8sG3Sm+Zs#==&4@Ld4D5xfS93W7r}Kd&>|W zd)OwOWBM_fxSlCBn{}Zc!m2K+7V7=#%}(Ezi@OFhqZ`FXv$R$X>Kv-ygqkGyq3cv4jb~ zoj4!$kn)c>=Sp0U0KdzApUC%3+lnLlwq183qI>Ojw%~W{^Z49-_UkhcJz)Pw zE}{qR+4ykGrw?C>=)3mcxN?5qo>_tD2X@YGM32~6QACg0^_&-7NURK@1lF0b3><{is-!1E;hjh zp?|VLE)7+li|DdYD?8xI(B!Wmx+-+f1VlH5t{aBv=Fqp#LG-oIiMtTp8oG*2erM=f z-n%Pw5AS_5G{By^JCx5-9tb_cs|Q2HXga}x;nf=fm_K&_;m+1A8am={e0A$2PCJ{Q zV5$8}^AHY9IH(5BCuH!cuOb|(k0IRl5#PA| zpWO&g>z#yf$B*(6?#yTBogTXZ;Tcl$F8c|NtF!FIyY&|xQb!~`{P1T{&60!HnsF`vhtwii}F-F z(5LRe-3CuG4qP-27U#&@;|>IR4(@y=mLRqfnVbD9Hkh6?)x`{ z%5h~`8_e@M#sHDuFddt6s&M`H&pzuh_1}|GE;;t-4BylF6Q9>$3j@*u%DeAh>Xgf^ zrK}Ww8}x(xMz)=K|5)C{Z#Din9hmpuesDRiEQ_Q!e*>nX>Qc(kNr^BMS)cjpKOtH! z@CjH?_}il*%hcbz$Hbd)|KGmnZ`aRLlZL-?3B5it_19qQG$dF>Q{M0O^S{^6KdLjD z_nYU<_wP=4{`N!5<%!!d$MN?l8wWo=k2Nl-{k{ws+trl6X>>WRENc^}8U9A9$PE*k z(;^Y;e}0#KewTiJpZPFdg8nSa#8{yN&qv3WOU|hNz!OQb_Pm`UjPGsJvz(@jiRC8d zJu=Pnuj}W}ndUDw`CU`fJm1WT1;34^Vbo<(T?^7Y|Kwiv!2X2sn^^ya`uW7~?6_Jz z|F;|Uixb{&%2}$P59YG0^_0utw`+Ltj(N^N8`C`hi)xi~UCiWEapLow<`bGoG8T2H zoEs7zNVt^tG;^Q-O=C}0Iq%j34VwsyB$L7Wu{ty7*HrI+`YiSQi3t;M;`?7shOD=p_HmFlu7xpCCK~^h~)QBs}CksAbl(Ap9`PtW!ZaHd7lm_(75mTSr)CUGd)xLlAG)iy(ZAW!8Zp{7B5}8~h+i zhpn-&dQ1f$XT8~$3O?R4^Q;u0gRn(vKKU26CL{v^30o7>z_IB|@e5m%Q$SfxEDd~0 z8hBO`+y*3seqW&JCzFBmLx%MiE)#(tzle$uiS3^QILq0PP|hL^-@cSkLKlZW>=M z&ujAC`VS3%AOZfChCip_o8&3W`cT7*k5c6nX!s`@9@p?v4bQ~l!}@d zuXpQuVrG%wES-Pcq;k17^mVDuzdzx7se8lnCr(!RUzDdTYpu?|Pv_UmoOO!M|Dn!* zpKfSwa9N*SI=|kYT4!naCu>#thTOPJm$Pn;f`jQJziTx7pBmnbcH!>^4gcNZa$Z`a zHT>%ueo2jjliuR*J`KNpNx58~Eum#SrQtJ|Dmcd#e=lqJE!pLA{hdsSthY3LO@V@Q zKgi#^fb)9?^!J+Y`j^gs%Hncnvvx>mSy2!HZ0CVAA*=O3o?oA&us z!~d-D%Iw2OVS-|NzMX(?Q#AYq4F`i#enlF7UqU(68h*Ei8+=Z;UaXP)Socp>_1DE) zae*hVBc}pxS%)XB`)5o3an|qKHZX(xyIA1K>pqpCSxzEdLH;S{&ux01GzC2%@ML=6 zdB6_?e!fswE?I%b@_PgDLou(8jc<@^T*~iV$*(Vb(Z^}vqtJjcUp|wZCGccAq!e(| zM0&a$Qho~qpn1)fabmZiyGC*|uxebFX?kGEdX_0-e9wJS|ISEPYo zp9X$c8u)X7M}g08wr%j$#^<=4enS4#fm{mb=$6CYk}SNY9% z-K*hmYPjjI9{`@}dtU}T6&}7N`A1qW>UHyD%)k7-lct=1rGbw`1ya3tS{it18u*el z@D+f^q-MdOJx%`8(!lqpf!~t`{=GEt=hDD`l?MJ^8u&i|PxW1g9>n$>X+5R;#jNAw z1s-ezUS$hBdB2H(Tv-oLvo9);Q*4pc}5#aimy3JOd?xaK1nfJihm|;*{=oI7aVp zZW-KWLH31%zHuT!UTOY3Iz>&9iS9Bxl}rtX91XxdqLRY34|aFcp_T7S97G4Q29Jwi zMqqh;`SiOF8>Zk=z`+RbchdH86=*`}8-9GwGgb{a-?hPD;qMd#A z!^aiQ)AF84=PJ^DwyURyhkNSBdbUD@S!k)x@mvSu^J|(KDp%of%I4<0qQXM9p$}40 zQeaM}j&JM4=kXAuuFlhVGz%IF|Iu;un(udZDvru|wlfcz*<#$4!qYF@f+iMUR6?g_ zu1C}0yK&$MZ~6{`O?;W_@- zL6+Ly(+$tyY)fksuISkm=Vss#a5%{dzNMsOUcLnk?uX}omeLk)?}R^8dUVofuqWg% zg){bGbC(tt0{Ockt!9(pe9pl(bpmcuzIoQEgPlD4h-bSe-YuGo?>f-qC3DSd#OauK z(r#i&bLsEaj}UY7-5RER_gox-mhePDLT{AJEi6gQgZ@c)swnBrC6Wgxe~MdG@i)qe zgdPm(dz4u1j$Qh`ZSU`CR$XQ_(;_BL!!!#Di`)JwwpnGSJfz ztSPI|)dCNcI6%9%x2qFAWvTff!`ZDKJ*g|_;Pg3&EYkQE&Vr(%gPV;Gf74BvaF8c1 z*l>ocI_pU_Em{vQQ-f7X^MU&09D3SII8w2hH6r zor&+4cGl}yN2+q+)74$+h>LKD2iN+T9|!y6?eaE$CJwf3?(d4nd%YH7C(3lfHj`dv zg_^f^4s4P&f(P~Zu#YI7u0ezSEw7Lfv86|*HFOTYRHJ+6b|{-;x2EI zqrKP)JTt&+7dc$8XS)E@o0bhVuhb7#!YeQ4SV12iVLi~-(iW!^y*{eJU@W%`4)k;b zwYR{@`&P`vJvigOlV}Xu0lGb{JzY|;w736FI4P#1bE9`puNWw)Gx$Alnr>8r_-XPH y{qe32^gPD7`M|&^=c=-dZvFTGKUln1T6*A!%Ro5x_0A5~=br$L;EFf+_Wun_O0QD@ literal 0 HcmV?d00001 diff --git a/examples/msg/mc/chord_liveness.c b/examples/msg/mc/chord/chord_liveness.c similarity index 99% rename from examples/msg/mc/chord_liveness.c rename to examples/msg/mc/chord/chord_liveness.c index 14c5214418..48563958ae 100644 --- a/examples/msg/mc/chord_liveness.c +++ b/examples/msg/mc/chord/chord_liveness.c @@ -942,7 +942,7 @@ int main(int argc, char *argv[]) MSG_config("model-check/property","promela_chord_liveness"); MC_automaton_new_propositional_symbol("join", &predJoin); - MSG_create_environment("../msg_platform.xml"); + MSG_create_environment("../../msg_platform.xml"); MSG_function_register("node", node); MSG_launch_application("deploy_chord_liveness.xml"); diff --git a/examples/msg/mc/chord_liveness.h b/examples/msg/mc/chord/chord_liveness.h similarity index 100% rename from examples/msg/mc/chord_liveness.h rename to examples/msg/mc/chord/chord_liveness.h diff --git a/examples/msg/mc/chord/deploy_chord_before_dsend_liveness.xml b/examples/msg/mc/chord/deploy_chord_before_dsend_liveness.xml new file mode 100644 index 0000000000..40b8ed9a46 --- /dev/null +++ b/examples/msg/mc/chord/deploy_chord_before_dsend_liveness.xml @@ -0,0 +1,31 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/msg/mc/deploy_chord_liveness.xml b/examples/msg/mc/chord/deploy_chord_liveness.xml similarity index 100% rename from examples/msg/mc/deploy_chord_liveness.xml rename to examples/msg/mc/chord/deploy_chord_liveness.xml diff --git a/examples/msg/mc/promela_chord_liveness b/examples/msg/mc/chord/promela_chord_liveness similarity index 100% rename from examples/msg/mc/promela_chord_liveness rename to examples/msg/mc/chord/promela_chord_liveness -- 2.20.1