Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
18 hours agocosmetics master
Martin Quinson [Sun, 19 Mar 2023 20:15:10 +0000 (21:15 +0100)]

18 hours agoMove more of the CheckerSide creation logic to the object constructor
Martin Quinson [Sun, 19 Mar 2023 20:07:00 +0000 (21:07 +0100)]
Move more of the CheckerSide creation logic to the object constructor

20 hours agoMC: disable Address Space Layout Randomization in the application
Martin Quinson [Sun, 19 Mar 2023 18:45:39 +0000 (19:45 +0100)]
MC: disable Address Space Layout Randomization in the application

This will allow to re-fork the application on restore without
invalidating all the metadata we accumulated in the previous
exploration traces.

23 hours agoDiffer the creation of the RemoteProcessMemory to when we have enough information
Martin Quinson [Sun, 19 Mar 2023 15:18:05 +0000 (16:18 +0100)]
Differ the creation of the RemoteProcessMemory to when we have enough information

23 hours agoBetter responsabilities splitup between CheckerSide and RemoteProcessMemory
Martin Quinson [Sun, 19 Mar 2023 14:57:19 +0000 (15:57 +0100)]
Better responsabilities splitup between CheckerSide and RemoteProcessMemory

24 hours agoMove methods not related to Memory out of RemoteProcessMemory
Martin Quinson [Sun, 19 Mar 2023 14:20:23 +0000 (15:20 +0100)]
Move methods not related to Memory out of RemoteProcessMemory

Now that ModelChecker is gone, it's time to move to the next step of cleanup.

The goal is that CheckerSide is in charge of the interaction with the
application process and RemoteProcessMemory is in charge of its memory.

Right now, RemoteProcessMemory does a bit more, as it stores the pid
and whether or not the application process is running.

This is bad because we want to make RemoteProcessMemory optional, only
used when we need to introspect the application memory (liveness
checking, non-progression checking, etc), so that we can run the app
in valgrind when we don't need to introspect its memory (safety
checking without non-progression checking).

I know I just moved this chunks of code from ModelChecker to
RemoteProcessMemory to now move it further, and I'm sorry for the
noise, but this code drives me nuts and I need to clean it step by step.

24 hours agoFinally kill the now empty ModelChecker class
Martin Quinson [Sun, 19 Mar 2023 14:01:44 +0000 (15:01 +0100)]
Finally kill the now empty ModelChecker class

25 hours agoMove the memory handling of RemoteProcessMemory singleton from ModelChecker to Checke...
Martin Quinson [Sun, 19 Mar 2023 13:50:37 +0000 (14:50 +0100)]
Move the memory handling of RemoteProcessMemory singleton from ModelChecker to CheckerSide

25 hours agoMove handle_message from ModelChecker to RemoteProcessMemory
Martin Quinson [Sun, 19 Mar 2023 13:29:05 +0000 (14:29 +0100)]
Move handle_message from ModelChecker to RemoteProcessMemory

25 hours agoMove handle_waitpid from ModelChecker to RemoteProcessMemory
Martin Quinson [Sun, 19 Mar 2023 12:54:23 +0000 (13:54 +0100)]
Move handle_waitpid from ModelChecker to RemoteProcessMemory

27 hours agoMake a global singleton of Exploration, to kill ModelChecker
Martin Quinson [Sun, 19 Mar 2023 11:46:57 +0000 (12:46 +0100)]
Make a global singleton of Exploration, to kill ModelChecker

Having global singletons is far from optimal, but it's a bit like the
EngineImpl singleton in the model-checker process.

This will allow to kill the ModelChecker class which responsabilities
were split between RemoteApp and Exploration.

27 hours agoGosh, how many calls to that global were there?
Martin Quinson [Sun, 19 Mar 2023 11:15:58 +0000 (12:15 +0100)]
Gosh, how many calls to that global were there?

27 hours agoKill a now unused class in mc
Martin Quinson [Sun, 19 Mar 2023 11:09:07 +0000 (12:09 +0100)]
Kill a now unused class in mc

27 hours agoRemove some more usage of mc_model_checker in Region and snapshoting logic
Martin Quinson [Sun, 19 Mar 2023 09:58:20 +0000 (10:58 +0100)]
Remove some more usage of mc_model_checker in Region and snapshoting logic

29 hours agoAnother use of mc_model_checker disapears. In Snapshot.equals.
Martin Quinson [Sun, 19 Mar 2023 09:10:34 +0000 (10:10 +0100)]
Another use of mc_model_checker disapears. In Snapshot.equals.

I guess that this could be done in a better way, as noted in the

30 hours agoanother mc_model_checker call location disappears
Martin Quinson [Sun, 19 Mar 2023 08:52:48 +0000 (09:52 +0100)]
another mc_model_checker call location disappears

I postponned this one a lot because it's impacting non-MC code, but at
the end it went smoothly

30 hours agoFix make distcheck
Martin Quinson [Sun, 19 Mar 2023 08:13:06 +0000 (09:13 +0100)]
Fix make distcheck

41 hours agoFix MC+clang builds
Martin Quinson [Sat, 18 Mar 2023 21:49:00 +0000 (22:49 +0100)]
Fix MC+clang builds

41 hours agoReduce a bit the adherance of handle_waitpid to ModelChecker
Martin Quinson [Sat, 18 Mar 2023 20:49:57 +0000 (21:49 +0100)]
Reduce a bit the adherance of handle_waitpid to ModelChecker

41 hours agoMerge branch 'master' into 'master'
Martin Quinson [Sat, 18 Mar 2023 21:21:14 +0000 (21:21 +0000)]
Merge branch 'master' into 'master'

First step for guided state

See merge request simgrid/simgrid!141

2 days agoMove DPOR and sleep set algorithm from backtrack to run procedure
mlaurent [Sat, 18 Mar 2023 14:58:43 +0000 (15:58 +0100)]
Move DPOR and sleep set algorithm from backtrack to run procedure

2 days agoMerge branch 'master' of https://framagit.org/simgrid/simgrid
mlaurent [Sat, 18 Mar 2023 13:48:00 +0000 (14:48 +0100)]
Merge branch 'master' of https://framagit.org/simgrid/simgrid

2 days agoReplace todo direct access with consider methods; guided or not
mlaurent [Sat, 18 Mar 2023 13:46:53 +0000 (14:46 +0100)]
Replace todo direct access with consider methods; guided or not

2 days agoBasicGuide handle next_transition if asked to
mlaurent [Sat, 18 Mar 2023 13:05:13 +0000 (14:05 +0100)]
BasicGuide handle next_transition if asked to

2 days agoMerge CheckerSide::start() intp the constructor
Martin Quinson [Sat, 18 Mar 2023 11:21:30 +0000 (12:21 +0100)]
Merge CheckerSide::start() intp the constructor

2 days agoBetter split of responsabilities between CheckerSide and RemoteApp
Martin Quinson [Sat, 18 Mar 2023 11:05:09 +0000 (12:05 +0100)]
Better split of responsabilities between CheckerSide and RemoteApp

Define in CheckerSide the callbacks that are used in there, instead of
defining it in the RemoteApp and passing it along to the CheckerSide.

Let's be optimistic: this code is every day a bit less messy.

2 days agoMove the checker_side_ from the ModelChecker to the RemoteApp
Martin Quinson [Sat, 18 Mar 2023 10:58:55 +0000 (11:58 +0100)]
Move the checker_side_ from the ModelChecker to the RemoteApp

with an axe.

2 days agoOne usage of mc_model_checker less
Martin Quinson [Sat, 18 Mar 2023 10:25:53 +0000 (11:25 +0100)]
One usage of mc_model_checker less

I had to reduce the const-ness of the RemoteProcessMemory variable in
Snapshot::operator==() because getting the heap modifies the
RemoteMemory object. Sorry sonar.

2 days agoAdd GuidedState abstract class; move ActorState management
mlaurent [Sat, 18 Mar 2023 10:14:35 +0000 (11:14 +0100)]
Add GuidedState abstract class; move ActorState management

2 days agoSimplify Channel::receive by handling non-blocking recv separately
Martin Quinson [Fri, 17 Mar 2023 22:02:27 +0000 (23:02 +0100)]
Simplify Channel::receive by handling non-blocking recv separately

2 days agoA few calls to mc_model_checker less by passing more parameters
Martin Quinson [Fri, 17 Mar 2023 21:23:09 +0000 (22:23 +0100)]
A few calls to mc_model_checker less by passing more parameters

2 days agoMove handle_simcall from ModelChecker to RemoteApp
Martin Quinson [Fri, 17 Mar 2023 21:13:40 +0000 (22:13 +0100)]
Move handle_simcall from ModelChecker to RemoteApp

2 days agoMerge branch 'master' into 'master'
Martin Quinson [Fri, 17 Mar 2023 21:42:38 +0000 (21:42 +0000)]
Merge branch 'master' into 'master'

Add reference to parent state

See merge request simgrid/simgrid!140

2 days agoAdd reference to parent state: only use this creation in DFSexplorer
mlaurent [Fri, 17 Mar 2023 15:55:22 +0000 (16:55 +0100)]
Add reference to parent state: only use this creation in DFSexplorer

4 days agoMissing include.
Arnaud Giersch [Thu, 16 Mar 2023 10:58:11 +0000 (11:58 +0100)]
Missing include.

4 days agoDecrease required version for nlohmann_json; add to jenkins/project_description.sh.
Arnaud Giersch [Thu, 16 Mar 2023 10:46:41 +0000 (11:46 +0100)]
Decrease required version for nlohmann_json; add to jenkins/project_description.sh.

Version 3.7.0 is available in debian/buster-backports.

4 days agoUseless guards.
Arnaud Giersch [Wed, 15 Mar 2023 14:25:52 +0000 (15:25 +0100)]
Useless guards.

4 days agoApply "smpi/buffering" when MC_record_replay_is_active too.
Arnaud Giersch [Wed, 15 Mar 2023 14:17:52 +0000 (15:17 +0100)]
Apply "smpi/buffering" when MC_record_replay_is_active too.

4 days agoSanitize how we know the current MC mode
Martin Quinson [Wed, 15 Mar 2023 22:54:52 +0000 (23:54 +0100)]
Sanitize how we know the current MC mode

This can be either NONE, AppSide, CheckerSide or Replay.

Also, further reduce how often we use the mc_model_checker singleton

4 days agoMake it compile with all warnings enabled
Martin Quinson [Wed, 15 Mar 2023 22:23:03 +0000 (23:23 +0100)]
Make it compile with all warnings enabled

4 days agoDocument a future cleanup to do when we bump cmake version
Martin Quinson [Wed, 15 Mar 2023 21:55:45 +0000 (22:55 +0100)]
Document a future cleanup to do when we bump cmake version

5 days agoRemove comments about non-existent support for smpi/privatization in MC.
Arnaud Giersch [Tue, 14 Mar 2023 15:51:08 +0000 (16:51 +0100)]
Remove comments about non-existent support for smpi/privatization in MC.


5 days agoReally check the privatization option in the MCed SMPI app.
Arnaud Giersch [Tue, 14 Mar 2023 15:34:28 +0000 (16:34 +0100)]
Really check the privatization option in the MCed SMPI app.

6 days agoInform if JSON lib is found.
Arnaud Giersch [Tue, 14 Mar 2023 08:24:44 +0000 (09:24 +0100)]
Inform if JSON lib is found.

6 days agoTest for JSON before using it
Martin Quinson [Mon, 13 Mar 2023 23:43:27 +0000 (00:43 +0100)]
Test for JSON before using it

6 days agoCosmetics
Martin Quinson [Mon, 13 Mar 2023 23:43:04 +0000 (00:43 +0100)]

6 days agofix make distcheck
Martin Quinson [Mon, 13 Mar 2023 21:47:12 +0000 (22:47 +0100)]
fix make distcheck

6 days agoMerge branch 'master' into 'master'
Fred Suter [Mon, 13 Mar 2023 21:12:47 +0000 (21:12 +0000)]
Merge branch 'master' into 'master'

Add wfformat json DAG loader and DAG doc

See merge request simgrid/simgrid!137

6 days agoAdd wfformat json DAG loader and DAG doc
Adrien [Mon, 13 Mar 2023 21:12:47 +0000 (21:12 +0000)]
Add wfformat json DAG loader and DAG doc

7 days agoCorrectly protect tests property settings, bummer
Martin Quinson [Mon, 13 Mar 2023 09:34:06 +0000 (10:34 +0100)]
Correctly protect tests property settings, bummer

7 days agoGive the remote_process_memory to the mc::State constructor
Martin Quinson [Mon, 13 Mar 2023 09:07:07 +0000 (10:07 +0100)]
Give the remote_process_memory to the mc::State constructor

This way, we rely a bit less on the ugly mc_model_checker singleton.

7 days agoMove another function of ModelChecker to RemoteProcessMemory
Martin Quinson [Sun, 12 Mar 2023 23:05:42 +0000 (00:05 +0100)]
Move another function of ModelChecker to RemoteProcessMemory

7 days agoMove another function out of ModelChecker
Martin Quinson [Sun, 12 Mar 2023 22:59:42 +0000 (23:59 +0100)]
Move another function out of ModelChecker

7 days agoMove a function from ModelChecker to Exploration
Martin Quinson [Sun, 12 Mar 2023 22:52:33 +0000 (23:52 +0100)]
Move a function from ModelChecker to Exploration

7 days agomove wait_for_requests() from ModelChecker to RemoteApp
Martin Quinson [Sun, 12 Mar 2023 22:31:40 +0000 (23:31 +0100)]
move wait_for_requests() from ModelChecker to RemoteApp

7 days agoInline a function in ModelChecker
Martin Quinson [Sun, 12 Mar 2023 22:10:10 +0000 (23:10 +0100)]
Inline a function in ModelChecker

7 days agoMove one method from ModelChecker to Exploration
Martin Quinson [Sun, 12 Mar 2023 22:05:06 +0000 (23:05 +0100)]
Move one method from ModelChecker to Exploration

7 days agoMove 2 functions from mc::ModelChecker to mc::RemoteApp
Martin Quinson [Sun, 12 Mar 2023 21:57:25 +0000 (22:57 +0100)]
Move 2 functions from mc::ModelChecker to mc::RemoteApp

7 days agoMake the sendsend tests at least fail fast to not hinder my workflow
Martin Quinson [Sun, 12 Mar 2023 21:35:53 +0000 (22:35 +0100)]
Make the sendsend tests at least fail fast to not hinder my workflow

7 days agoMC: rename remote/RemoteProcess to sosp/RemoteProcessMemory
Martin Quinson [Sun, 12 Mar 2023 21:16:16 +0000 (22:16 +0100)]
MC: rename remote/RemoteProcess to sosp/RemoteProcessMemory

7 days agoClean leftovers
Martin Quinson [Sun, 12 Mar 2023 20:50:18 +0000 (21:50 +0100)]
Clean leftovers

7 days agoMC: stop reading maxpid in memory, but ask it over the network instead
Martin Quinson [Sat, 11 Mar 2023 00:05:31 +0000 (01:05 +0100)]
MC: stop reading maxpid in memory, but ask it over the network instead

7 days agoOne use less of the global mc_model_checker
Martin Quinson [Fri, 10 Mar 2023 22:44:05 +0000 (23:44 +0100)]
One use less of the global mc_model_checker

7 days agoThis seems to reduce the amount of failure, but I don't know why :(
Martin Quinson [Fri, 10 Mar 2023 22:34:07 +0000 (23:34 +0100)]
This seems to reduce the amount of failure, but I don't know why :(

Not sure I know what I'm doing here :(

7 days agoFix build with -D_GLIBCXX_DEBUG [-Werror=range-loop-construct].
Arnaud Giersch [Sun, 12 Mar 2023 15:16:23 +0000 (16:16 +0100)]
Fix build with -D_GLIBCXX_DEBUG [-Werror=range-loop-construct].

9 days agoFix assert: min and max are both included in interval for MC_random.
Arnaud Giersch [Fri, 10 Mar 2023 16:08:07 +0000 (17:08 +0100)]
Fix assert: min and max are both included in interval for MC_random.


9 days agoMerge branch 'udpor-phase5' into 'master'
Martin Quinson [Fri, 10 Mar 2023 21:25:15 +0000 (21:25 +0000)]
Merge branch 'udpor-phase5' into 'master'

Phase 5 of UDPOR Integration: Implementing Conflict Checks

See merge request simgrid/simgrid!138

9 days agoTry to avoid a segfault on assert message
Martin Quinson [Fri, 10 Mar 2023 18:48:33 +0000 (19:48 +0100)]
Try to avoid a segfault on assert message

This is an attempt to fix https://framagit.org/simgrid/simgrid/-/issues/118

10 days agoAdd first test for immediate conflicts edge case
Maxwell Pirtle [Fri, 10 Mar 2023 10:15:36 +0000 (11:15 +0100)]
Add first test for immediate conflicts edge case

Detecting immediate conflicts is much more subtle
than detecting conflicts in general. The subtlety
lies in the fact that the collection of events
in the shared history of the two events under
consideration must itself be a valid configuration:
in other words, the events would not be considered
to be in immediate conflict if somewhere in their
history lies a conflict.

10 days agoAdd first batch of tests for conflict detection among events
Maxwell Pirtle [Fri, 10 Mar 2023 09:06:33 +0000 (10:06 +0100)]
Add first batch of tests for conflict detection among events

Detecting conflicts among a collection of events
is super critical to the proper functioning of
UDPOR (it is primarily used to compute en(C) for
a given configuration). Testing conflicts among
events in an event structure is very important.
Subsequent commits and MRs will continue to add
tests for detecting conflicts among collections
of events.

Detecting immediate conflicts is also critical
when it comes to determining which events UDPOR
decides to keep around after continuing its search.
Immediate conflicts are more subtle and should be
tested with great care.

10 days agore-fixed assert message with up-to-date configuration option name
Henri Casanova [Thu, 9 Mar 2023 19:08:18 +0000 (09:08 -1000)]
re-fixed assert message with up-to-date configuration option name

10 days agoAssert message fix
Henri Casanova [Thu, 9 Mar 2023 18:45:19 +0000 (08:45 -1000)]
Assert message fix

11 days agoAdd implementation for immediate conflicts
Maxwell Pirtle [Thu, 9 Mar 2023 14:34:25 +0000 (15:34 +0100)]
Add implementation for immediate conflicts

Two events are said to be in immediate conflict
if they are conflicting but if the removal of
either event from their shared history would
result in a conflict-free set. That is, if
the only conflict among the set of events in
the history of the two events `e` and `e'`
is between `e` and `e'`, then `e` and `e'`
are in immediate conflict

11 days agoRequire conflict-freedom in is_valid_configuration
Maxwell Pirtle [Thu, 9 Mar 2023 14:19:07 +0000 (15:19 +0100)]
Require conflict-freedom in is_valid_configuration

The method `EventSet::is_valid_configuration()`
was missing the condition that the set of events
need also be free of conflicts (in addition to
being causally closed)

11 days agoAdd src/.../udpor/udpor_tests_private.hpp to CMake
Maxwell Pirtle [Thu, 9 Mar 2023 13:18:56 +0000 (14:18 +0100)]
Add src/.../udpor/udpor_tests_private.hpp to CMake

11 days agoEager mode is for the first case only (thx adegomme).
Arnaud Giersch [Thu, 9 Mar 2023 13:18:32 +0000 (14:18 +0100)]
Eager mode is for the first case only (thx adegomme).


11 days agoAdd test to verify topological ordering of EventSet
Maxwell Pirtle [Thu, 9 Mar 2023 13:08:27 +0000 (14:08 +0100)]
Add test to verify topological ordering of EventSet

The topological ordering was moved into EventSet
in a prior commit since it is useful to order
events in an EventSet that reside outside of a
Configuration. This commit adds a stress test
that verifies that the topological orderings
of all possible subsets of a collection of
events obey the topological ordering invariant
after being ordered (in both directions)

11 days agoImprove doc for smpi/buffering.
Arnaud Giersch [Thu, 9 Mar 2023 10:36:49 +0000 (11:36 +0100)]
Improve doc for smpi/buffering.

Describe the behavior like for smpi/send-is-detached-thresh.

11 days agoFix asserts for when received size is 0 (message type is invalid).
Arnaud Giersch [Wed, 8 Mar 2023 22:15:18 +0000 (23:15 +0100)]
Fix asserts for when received size is 0 (message type is invalid).

11 days agoDepreciate unused functions s4u::Comm::copy_{buffer,pointer}_callback().
Arnaud Giersch [Wed, 8 Mar 2023 15:36:45 +0000 (16:36 +0100)]
Depreciate unused functions s4u::Comm::copy_{buffer,pointer}_callback().

11 days agoInline s4u::Comm::copy_pointer_callback which is the default callback.
Arnaud Giersch [Wed, 8 Mar 2023 15:36:13 +0000 (16:36 +0100)]
Inline s4u::Comm::copy_pointer_callback which is the default callback.

12 days agoBegin filling in computations of ex(C) and en(C)
Maxwell Pirtle [Wed, 8 Mar 2023 14:27:43 +0000 (15:27 +0100)]
Begin filling in computations of ex(C) and en(C)

This commit introduces the first steps towards
computing ex(C) and en(C) using many of the
additions of the previous phases. An important
part of the computation is so far missing, however,
viz. the determination of whether or not an action
`a` is enabled at some point in the past. We'll
need to decipher what's going on in tiny_simgrid
to fully determine what to do here; for now, we
simply ignore adding an event entirely and just
say that `a` was disabled at all points in the past.

12 days agoDepreciate ForcefulKillException::try_n_catch().
Arnaud Giersch [Wed, 8 Mar 2023 14:09:13 +0000 (15:09 +0100)]
Depreciate ForcefulKillException::try_n_catch().

It was used by the Java bindings.

12 days agoObvious typo.
Arnaud Giersch [Wed, 8 Mar 2023 13:23:00 +0000 (14:23 +0100)]
Obvious typo.

12 days agoFix logic for mutual conflict between two events
Maxwell Pirtle [Wed, 8 Mar 2023 13:11:39 +0000 (14:11 +0100)]
Fix logic for mutual conflict between two events

Prior to this commit, detecting whether two
events were in conflict involved looking at all
of the events with respect to all others. However,
you must instead *only* look at how the event `e`
and `e'` relate to the other event's history:
we wouldn't care if some other event is in conflict
with `e'` if `e` is not that event

12 days agoAdd conflict-free invariant check to Configuration
Maxwell Pirtle [Wed, 8 Mar 2023 12:12:00 +0000 (13:12 +0100)]
Add conflict-free invariant check to Configuration

When adding events to a configuration, we want to
ensure that the configuration remains both a)
causally closed and b) conflict-free. The latter
required that the tests be modified as they effectively
assumed that the transitions associated with each
event were independent of one another. Since the
`Transition` base class is dependent by default, this
was at odds with the assumptions

12 days agoUse #include <...> for foreign header files.
Arnaud Giersch [Wed, 8 Mar 2023 10:23:17 +0000 (11:23 +0100)]
Use #include <...> for foreign header files.

Files in teshsuite/smpi/mpich3-test/ were not considered.

12 days agoAdd preliminary tests for checking event conflicts
Maxwell Pirtle [Wed, 8 Mar 2023 10:18:50 +0000 (11:18 +0100)]
Add preliminary tests for checking event conflicts

12 days agoAdd conflict detection to EventSet
Maxwell Pirtle [Wed, 8 Mar 2023 08:13:15 +0000 (09:13 +0100)]
Add conflict detection to EventSet

Detecting whether or not a collection of events
are in conflict important for computing en(C)
and for K-partial alternatives. We simply
follow the definition of conflicts. More
esoteric methods may exist that are faster,
but for now let's keep it simple: we can always
add those in later incrementally

12 days agoMerge branch 'udpor-phase4' into 'master'
Martin Quinson [Wed, 8 Mar 2023 00:10:15 +0000 (00:10 +0000)]
Merge branch 'udpor-phase4' into 'master'

Phase 4 of UDPOR Integration: Variable For-loop

See merge request simgrid/simgrid!136

13 days agoAdd ability to restrict maximum subset size
Maxwell Pirtle [Tue, 7 Mar 2023 13:36:03 +0000 (14:36 +0100)]
Add ability to restrict maximum subset size

This commit adds the ability to restrict the
size of the maximal subsets that are produced
by the maximal_subsets_iterator. This filtering
significantly reduces the number of subsets that
need to be searched in more complicated graphs.

The advantage of adding the filtering directly
to the maximal_subsets_iterator over using a
higher-order iterator such as boost::filter_iterator
is that branches can be pruned immediately. Since
the maximal_subsets_iterator performs its search
in depth-first order, something like
boost::filter_iterator, while technically equivalent,
would have to actually perform the iteration over
entire branches that are otherwise useless due to
their size.

Searching maximal subsets of a restricted size is
useful when determining conflicts between sets of
events: we want to look at pairs of maximal events

13 days agoAdd asserts for Configuration vs EventSet
Maxwell Pirtle [Tue, 7 Mar 2023 13:05:01 +0000 (14:05 +0100)]
Add asserts for Configuration vs EventSet

This commit adds two asserts to ensure that
traversing a configuration is equivalent to
traversing the events of that configuration.
That is, the assertions check that a configuration
can effectively be treated as a set of events
when it comes to traversal of maximal sets and
computing a topological ordering

13 days agoAllow iteration over maximal subsets of an EventSet
Maxwell Pirtle [Tue, 7 Mar 2023 12:48:29 +0000 (13:48 +0100)]
Allow iteration over maximal subsets of an EventSet

The maximal_subsets_iterator was updated to allow
traversal over the subsets of events of some set `E`
which are maximal (i.e. causally-free). It is a
simple addition which extends the power of the iterator
to EventSets more generally (as opposed to strictly
for Configurations)

13 days agoMove topological ordering to EventSet
Maxwell Pirtle [Tue, 7 Mar 2023 12:41:41 +0000 (13:41 +0100)]
Move topological ordering to EventSet

The events of an EventSet can be ordered
topologically by considering them as part
of the configuration containing the histories
of all events in the set. The trick is to
ignore adding in an event into the ordering
if the event is not contained in the original
set itself

13 days agoRename `EventSet::is_maximal_event_set()`
Maxwell Pirtle [Tue, 7 Mar 2023 09:05:45 +0000 (10:05 +0100)]
Rename `EventSet::is_maximal_event_set()`

The method `is_maximal_event_set()` was renamed
to simply `is_maximal()`, since the question is
already being asked about some event set (i.e.
the `_event_set` bit is redundant)

13 days agoAdd some basic tests for variable_for_loop
Maxwell Pirtle [Tue, 7 Mar 2023 08:10:58 +0000 (09:10 +0100)]
Add some basic tests for variable_for_loop

Some tests were added to confirm that the
variable_for_loop iterator behaved as expected.

13 days agoFixes in docs/source/tuto_* (untested).
Arnaud Giersch [Mon, 6 Mar 2023 15:16:49 +0000 (16:16 +0100)]
Fixes in docs/source/tuto_* (untested).

13 days agoWrite maximal_subsets_iterator_wrapper with xbt utils
Maxwell Pirtle [Mon, 6 Mar 2023 15:13:50 +0000 (16:13 +0100)]
Write maximal_subsets_iterator_wrapper with xbt utils

2 weeks agoFix edge cases in variable_for_loop
Maxwell Pirtle [Mon, 6 Mar 2023 14:28:05 +0000 (15:28 +0100)]
Fix edge cases in variable_for_loop

Some tests were added which detected an off-by-one
error in the implementation logic of the variable_for_loop.
Subsequent commits will add more tests to the iterator
for further verification

2 weeks agoWrite LazyPowerSet in terms of iterator_wrapper
Maxwell Pirtle [Mon, 6 Mar 2023 13:41:24 +0000 (14:41 +0100)]
Write LazyPowerSet in terms of iterator_wrapper