Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
simgrid.git
12 months agoFactorize more code between DFSExplo and LivenessExplo, and UDPOR
Martin Quinson [Thu, 27 Apr 2023 23:25:04 +0000 (01:25 +0200)]
Factorize more code between DFSExplo and LivenessExplo, and UDPOR

12 months agoKill useless empty function.
Arnaud Giersch [Tue, 2 May 2023 14:32:11 +0000 (16:32 +0200)]
Kill useless empty function.

12 months agoMissing "override".
Arnaud Giersch [Tue, 2 May 2023 14:22:02 +0000 (16:22 +0200)]
Missing "override".

12 months agoSimplify expression.
Arnaud Giersch [Tue, 2 May 2023 14:14:43 +0000 (16:14 +0200)]
Simplify expression.

12 months agoFix use-after-free observed with the s4u-operation examples.
Arnaud Giersch [Tue, 2 May 2023 14:12:18 +0000 (16:12 +0200)]
Fix use-after-free observed with the s4u-operation examples.

12 months agoCosmetics (sonar).
Arnaud Giersch [Tue, 2 May 2023 14:24:29 +0000 (16:24 +0200)]
Cosmetics (sonar).

12 months agoDefine each identifier in a dedicated statement (sonar).
Arnaud Giersch [Tue, 11 Apr 2023 09:13:59 +0000 (11:13 +0200)]
Define each identifier in a dedicated statement (sonar).

12 months agoRevert "Run mc-*-liveness tests serial, and hope to pass on CI."
Arnaud Giersch [Sat, 29 Apr 2023 08:03:02 +0000 (10:03 +0200)]
Revert "Run mc-*-liveness tests serial, and hope to pass on CI."

This reverts commit 881507dc9fbeba0c63112dd0058d9c591b67419e.

In fact, it was just the CI infrastructure that was unusually slow these days.

12 months agoWhitespace cleanup (codefactor.io).
Arnaud Giersch [Tue, 18 Apr 2023 09:39:48 +0000 (11:39 +0200)]
Whitespace cleanup (codefactor.io).

12 months agoLazily compute the recipe of a state, on need only
Martin Quinson [Thu, 27 Apr 2023 13:41:03 +0000 (15:41 +0200)]
Lazily compute the recipe of a state, on need only

This will be useful when leveraging intermediate states during
backtracks. In that case, we need to compute partial recipes, up to
the advanced restaure point.

12 months agoMore automatic memory mgmt in MC
Martin Quinson [Thu, 27 Apr 2023 12:09:03 +0000 (14:09 +0200)]
More automatic memory mgmt in MC

12 months agoMC: give each state an incoming transition too
Martin Quinson [Thu, 27 Apr 2023 11:48:19 +0000 (13:48 +0200)]
MC: give each state an incoming transition too

Using the parent's outgoing transition is not reliable anymore now
that we don't always explore the tree in order, but rather following
the exploration strategies.

12 months agoFix comment [no-ci]
Martin Quinson [Tue, 18 Apr 2023 07:01:51 +0000 (09:01 +0200)]
Fix comment [no-ci]

12 months agoRun mc-*-liveness tests serial, and hope to pass on CI.
Arnaud Giersch [Thu, 27 Apr 2023 12:57:19 +0000 (14:57 +0200)]
Run mc-*-liveness tests serial, and hope to pass on CI.

12 months agoFix comment.
Arnaud Giersch [Thu, 27 Apr 2023 09:28:08 +0000 (11:28 +0200)]
Fix comment.

12 months agoThere is no need to declare the default constructors here.
Arnaud Giersch [Thu, 27 Apr 2023 09:27:02 +0000 (11:27 +0200)]
There is no need to declare the default constructors here.

12 months agoFix build error: exception specification of explicitly
Arnaud Giersch [Thu, 27 Apr 2023 09:26:20 +0000 (11:26 +0200)]
Fix build error: exception specification of explicitly
defaulted move constructor does not match the calculated one.

12 months agoMerge branch 'operation-plugin' into 'master'
Martin Quinson [Wed, 26 Apr 2023 12:45:40 +0000 (12:45 +0000)]
Merge branch 'operation-plugin' into 'master'

Operation plugin

See merge request simgrid/simgrid!145

13 months agoMerge branch 'udpor-phase7' into 'master'
Martin Quinson [Tue, 18 Apr 2023 07:08:17 +0000 (07:08 +0000)]
Merge branch 'udpor-phase7' into 'master'

Phase 7 of UDPOR Integration: Add specialized `ex(C)` computation for `Comm*` transitions

See merge request simgrid/simgrid!144

13 months agosonar fixes
Martin Quinson [Mon, 17 Apr 2023 08:01:01 +0000 (10:01 +0200)]
sonar fixes

- Undefined return value (that would happen on a platform without any host)
- Local variable shadowing
- Automatic memory management
- const, explicit, etc.

13 months agoLet resource profiles finish their initialization by themselves and kill presolve
Martin Quinson [Sun, 16 Apr 2023 16:45:59 +0000 (18:45 +0200)]
Let resource profiles finish their initialization by themselves and kill presolve

13 months agoNo need to presolve the models to finish their initialization nowadays
Martin Quinson [Sun, 16 Apr 2023 16:31:13 +0000 (18:31 +0200)]
No need to presolve the models to finish their initialization nowadays

I think that this was a leftover of the good old C times.

13 months agoOnly fire on_platform_created after creating the platform, not after loading the...
Martin Quinson [Sun, 16 Apr 2023 10:23:18 +0000 (12:23 +0200)]
Only fire on_platform_created after creating the platform, not after loading the deployment

13 months agoAdd a target to recompile all ns3 tests (and only them)
Martin Quinson [Sun, 16 Apr 2023 09:03:31 +0000 (11:03 +0200)]
Add a target to recompile all ns3 tests (and only them)

13 months agorename create to init. add init with name only. add setters
Adrien Gougeon [Sun, 16 Apr 2023 08:41:16 +0000 (10:41 +0200)]
rename create to init. add init with name only. add setters

13 months agoMake sure that we never have a 0 transition at the end of the stack
Martin Quinson [Sat, 15 Apr 2023 22:38:08 +0000 (00:38 +0200)]
Make sure that we never have a 0 transition at the end of the stack

13 months agoAlso send the disabled transitions over: UDPOR needs it
Martin Quinson [Sat, 15 Apr 2023 21:50:48 +0000 (23:50 +0200)]
Also send the disabled transitions over: UDPOR needs it

13 months agoMore informative message on system error
Martin Quinson [Sat, 15 Apr 2023 21:40:11 +0000 (23:40 +0200)]
More informative message on system error

13 months agoMore defensive programing style
Martin Quinson [Fri, 14 Apr 2023 12:21:47 +0000 (14:21 +0200)]
More defensive programing style

13 months agoadd missing '&' causing temporary value to be modified
Adrien Gougeon [Fri, 14 Apr 2023 10:37:41 +0000 (12:37 +0200)]
add missing '&' causing temporary value to be modified

13 months agorename on_start/on_end functions call to on_this_start/on_this_end. add on_start_cb...
Adrien Gougeon [Fri, 14 Apr 2023 09:24:00 +0000 (11:24 +0200)]
rename on_start/on_end functions call to on_this_start/on_this_end. add on_start_cb and on_end_cb

13 months agoTrust the config system to check that only valid values are used
Martin Quinson [Thu, 13 Apr 2023 21:51:41 +0000 (23:51 +0200)]
Trust the config system to check that only valid values are used

13 months agoDisable coverage on circleci.
Arnaud Giersch [Wed, 12 Apr 2023 20:02:34 +0000 (22:02 +0200)]
Disable coverage on circleci.

It seems that it is not used and it slows down the tests.

[ci-skip]

13 months agoMake this example valgrind-clean
Martin Quinson [Wed, 12 Apr 2023 20:46:30 +0000 (22:46 +0200)]
Make this example valgrind-clean

13 months agoFurther cosmetics in that example, adding a helper function to s4u on the way
Martin Quinson [Wed, 12 Apr 2023 19:37:05 +0000 (21:37 +0200)]
Further cosmetics in that example, adding a helper function to s4u on the way

13 months agosimplify the example now that host can be set to serial
Fred Suter [Wed, 12 Apr 2023 18:19:28 +0000 (14:19 -0400)]
simplify the example now that host can be set to serial

13 months agoUse host->set_concurrency_limit(1) in an example where it makes sense
Martin Quinson [Wed, 12 Apr 2023 15:58:18 +0000 (17:58 +0200)]
Use host->set_concurrency_limit(1) in an example where it makes sense

13 months agoDocument a bit the MC changes
Martin Quinson [Wed, 12 Apr 2023 15:49:30 +0000 (17:49 +0200)]
Document a bit the MC changes

13 months agoAllow to set a concurrency limit on disks and hosts
Martin Quinson [Wed, 12 Apr 2023 15:43:10 +0000 (17:43 +0200)]
Allow to set a concurrency limit on disks and hosts

13 months agoInline Exploration::system_error.
Arnaud Giersch [Wed, 12 Apr 2023 12:25:33 +0000 (14:25 +0200)]
Inline Exploration::system_error.

13 months agoRemove useless specialized exceptions from simgrid::mc.
Arnaud Giersch [Wed, 12 Apr 2023 12:23:15 +0000 (14:23 +0200)]
Remove useless specialized exceptions from simgrid::mc.

13 months agoUse an exception on Exploration::system_exit().
Arnaud Giersch [Wed, 12 Apr 2023 12:08:34 +0000 (14:08 +0200)]
Use an exception on Exploration::system_exit().

The goal is to use RAII to free the memory on exit, and get cleaner valgrind reports.

13 months agoSonar...
Arnaud Giersch [Wed, 12 Apr 2023 09:38:20 +0000 (11:38 +0200)]
Sonar...

13 months agomissing virtual destructor
Adrien Gougeon [Wed, 12 Apr 2023 07:59:11 +0000 (09:59 +0200)]
missing virtual destructor

13 months agofix distcheck
Adrien Gougeon [Tue, 11 Apr 2023 21:39:40 +0000 (23:39 +0200)]
fix distcheck

13 months agomissing lib
Adrien Gougeon [Tue, 11 Apr 2023 21:18:36 +0000 (23:18 +0200)]
missing lib

13 months agoclang-format
Adrien Gougeon [Tue, 11 Apr 2023 14:33:21 +0000 (16:33 +0200)]
clang-format

13 months agoadd prog_ns3 to manifest
Adrien Gougeon [Tue, 11 Apr 2023 14:30:27 +0000 (16:30 +0200)]
add prog_ns3 to manifest

13 months agoadd operation examples
Adrien Gougeon [Tue, 11 Apr 2023 13:48:40 +0000 (15:48 +0200)]
add operation examples

13 months agoseveral updates to plugin operation
Adrien Gougeon [Tue, 11 Apr 2023 13:48:13 +0000 (15:48 +0200)]
several updates to plugin operation

13 months agoadd operation to plugin doc
Adrien Gougeon [Tue, 11 Apr 2023 13:44:56 +0000 (15:44 +0200)]
add operation to plugin doc

13 months agoadd operation to manifest
Adrien Gougeon [Tue, 11 Apr 2023 13:43:43 +0000 (15:43 +0200)]
add operation to manifest

13 months agofix bad type comparison
Adrien Gougeon [Fri, 7 Apr 2023 09:00:05 +0000 (11:00 +0200)]
fix bad type comparison

13 months agoadd operation plugin
Adrien Gougeon [Wed, 5 Apr 2023 11:52:22 +0000 (13:52 +0200)]
add operation plugin

13 months agoAssignment operators should return non-"const" references (sonar).
Arnaud Giersch [Tue, 11 Apr 2023 13:26:28 +0000 (15:26 +0200)]
Assignment operators should return non-"const" references (sonar).

Also enfore C++ "rule-of-three".

13 months agoMark functions as "const" (sonar).
Arnaud Giersch [Tue, 11 Apr 2023 13:26:28 +0000 (15:26 +0200)]
Mark functions as "const" (sonar).

13 months agoUse std::string (sonar).
Arnaud Giersch [Tue, 11 Apr 2023 13:26:28 +0000 (15:26 +0200)]
Use std::string (sonar).

13 months agoMisc sonar issues.
Arnaud Giersch [Tue, 11 Apr 2023 13:26:28 +0000 (15:26 +0200)]
Misc sonar issues.

13 months agoReduce scope for variables (sonar).
Arnaud Giersch [Tue, 11 Apr 2023 13:26:28 +0000 (15:26 +0200)]
Reduce scope for variables (sonar).

13 months agoPointer and reference should be "const" if the corresponding object is not modified...
Arnaud Giersch [Tue, 11 Apr 2023 13:26:28 +0000 (15:26 +0200)]
Pointer and reference should be "const" if the corresponding object is not modified (sonar).

13 months agoFix bound checking in assert.
Arnaud Giersch [Tue, 11 Apr 2023 13:26:28 +0000 (15:26 +0200)]
Fix bound checking in assert.

13 months agoWhitespace cleanup (codefactor.io).
Arnaud Giersch [Tue, 11 Apr 2023 13:26:28 +0000 (15:26 +0200)]
Whitespace cleanup (codefactor.io).

13 months agoUse an intermediate variable to compute the sum and access c[i][j] only once.
Arnaud Giersch [Mon, 10 Apr 2023 20:03:39 +0000 (22:03 +0200)]
Use an intermediate variable to compute the sum and access c[i][j] only once.

May fix crash when built with Intel(R) oneAPI DPC++/C++ Compiler 2023.1.0 (2023.1.0.20230320)
Probably an optimization bug!

Also clean up the function signature.

13 months agoLess low-level operations to manage receive buffer.
Arnaud Giersch [Wed, 5 Apr 2023 20:04:58 +0000 (22:04 +0200)]
Less low-level operations to manage receive buffer.

13 months agoPlease don't fix this error reported by clang-static [no-ci]
Martin Quinson [Fri, 7 Apr 2023 20:05:40 +0000 (22:05 +0200)]
Please don't fix this error reported by clang-static [no-ci]

13 months agoDefine and use VALGRIND_NO_TRACE_CHILDREN for simgrid-mc tests.
Arnaud Giersch [Fri, 7 Apr 2023 16:52:53 +0000 (18:52 +0200)]
Define and use VALGRIND_NO_TRACE_CHILDREN for simgrid-mc tests.

There are two benefits. First, memory leaks are checked for the simgrid-mc process,
and then the tests run faster.

[ci-skip]

13 months agoAdd $VALGRIND_NO_LEAK_CHECK in tesh files when simgrid-mc is used.
Arnaud Giersch [Fri, 7 Apr 2023 14:49:36 +0000 (16:49 +0200)]
Add $VALGRIND_NO_LEAK_CHECK in tesh files when simgrid-mc is used.

Too many memory leaks are detected in the MCed processes.

13 months agoPass include and library directories to try_compile.
Arnaud Giersch [Fri, 7 Apr 2023 13:23:05 +0000 (15:23 +0200)]
Pass include and library directories to try_compile.

13 months agoFix usage of option --cfg=path in tesh files.
Arnaud Giersch [Fri, 7 Apr 2023 09:43:02 +0000 (11:43 +0200)]
Fix usage of option --cfg=path in tesh files.

Most of them reference a non-existent directory: examples/smpi/msg/.
Remove them.

Use the option in tests from basic-parsing-test.

13 months agoMake distcheck
Martin Quinson [Thu, 6 Apr 2023 16:08:07 +0000 (18:08 +0200)]
Make distcheck

13 months agoMC: Reap all zombie childs to avoid them to accumulate
Martin Quinson [Thu, 6 Apr 2023 15:48:05 +0000 (17:48 +0200)]
MC: Reap all zombie childs to avoid them to accumulate

13 months agoRemove the timings of another ns3 test to help older ns3 versions
Martin Quinson [Thu, 6 Apr 2023 14:58:39 +0000 (16:58 +0200)]
Remove the timings of another ns3 test to help older ns3 versions

13 months agoAllow ns3 to be idempotent if correctly patched
Martin Quinson [Thu, 6 Apr 2023 14:28:33 +0000 (16:28 +0200)]
Allow ns3 to be idempotent if correctly patched

13 months agoRename `remove()` method on `Unfolding`
Maxwell Pirtle [Thu, 6 Apr 2023 11:52:50 +0000 (13:52 +0200)]
Rename `remove()` method on `Unfolding`

Since the events aren't ever removed from the
Unfolding and are instead simply displaced,
we change the name of the method to better
reflect what is going on

13 months agoMake use of the sets `G` and `U` with `Unfolding`
Maxwell Pirtle [Thu, 6 Apr 2023 09:46:03 +0000 (11:46 +0200)]
Make use of the sets `G` and `U` with `Unfolding`

The `Unfolding` class in UDPOR previously discarded
all events from `U` when they were no longer needed.
Technically, UDPOR moves those events into a set `G`
which can be used to do more interesting things
in the future (e.g. to model check cyclic state spaces).
Furthermore, there are some subtlties it seems in
fully destroying the contents of an event after it has
been discovered, viz. with dealing with what to do when
a previous extension set contains such a deleted event

13 months agoFix bug with immediate conflict detection
Maxwell Pirtle [Wed, 5 Apr 2023 12:58:29 +0000 (14:58 +0200)]
Fix bug with immediate conflict detection

Detecting immediate conflicts for an event is
important as part of the clean up phase of
UDPOR. There was a typo that gave incorrect
results for the actual conflicts that were
detected which was resolved.

NOTE: There is still a problem with event
deletion. The issue is that previous configurations
will contain references to events which have been
deleted in the extension set which is computed
for them (ex(C)). I'm not quite sure how to
handle this at the moment...

13 months agoImprove the logging level of that message that is relatively important
Martin Quinson [Wed, 5 Apr 2023 20:38:06 +0000 (22:38 +0200)]
Improve the logging level of that message that is relatively important

13 months agothese ns3 tests need an 'output sort' directive :(
Martin Quinson [Wed, 5 Apr 2023 20:02:59 +0000 (22:02 +0200)]
these ns3 tests need an 'output sort' directive :(

13 months agoRegenerate tesh files (one more time).
Arnaud Giersch [Wed, 5 Apr 2023 15:28:29 +0000 (17:28 +0200)]
Regenerate tesh files (one more time).

13 months agoExamine all opened_states_ to find the best candidate.
Arnaud Giersch [Wed, 5 Apr 2023 14:26:27 +0000 (16:26 +0200)]
Examine all opened_states_ to find the best candidate.

We cannot use a std::multiset, nor a std::priority_queue as before since
the value for the priority may change, even for states already stored in
opeened_states_.

Citing mlaurent:
 "Le problème c'est que dans run() la partie gestion de "persistent set" peut
  modifier des acteurs de State déjà dans opened_states_ en les passant à Todo.
  Et ça, ça peut modifier la valeur renvoyée par next_transition_guided()."

13 months agoCosmetics.
Arnaud Giersch [Sun, 2 Apr 2023 09:43:45 +0000 (11:43 +0200)]
Cosmetics.

13 months agoRename MC_NEED_PTRACE -> SIMGRID_MC_NEED_PTRACE for consistency.
Arnaud Giersch [Tue, 4 Apr 2023 12:02:40 +0000 (14:02 +0200)]
Rename MC_NEED_PTRACE -> SIMGRID_MC_NEED_PTRACE for consistency.

13 months agoCentralize definitions for the name of environment variables used by the MC.
Arnaud Giersch [Thu, 30 Mar 2023 12:58:09 +0000 (14:58 +0200)]
Centralize definitions for the name of environment variables used by the MC.

13 months agoSonar smells; remove redundant mentions of std::shared_ptr<State>.
Arnaud Giersch [Wed, 5 Apr 2023 12:09:45 +0000 (14:09 +0200)]
Sonar smells; remove redundant mentions of std::shared_ptr<State>.

13 months agoFix make distcheck, stupid bummer
Martin Quinson [Wed, 5 Apr 2023 19:40:32 +0000 (21:40 +0200)]
Fix make distcheck, stupid bummer

13 months agoEnforce the ns3 timings for the latest version of ns3, and just execute older versions
Martin Quinson [Wed, 5 Apr 2023 19:27:39 +0000 (21:27 +0200)]
Enforce the ns3 timings for the latest version of ns3, and just execute older versions

13 months agoFix conflict detection between configs + history
Maxwell Pirtle [Wed, 5 Apr 2023 08:04:18 +0000 (10:04 +0200)]
Fix conflict detection between configs + history

The computation of K-partial alternatives requires
that we can determine whether or not `[e] + C`
for some event `e` is a valid configuration. There
was a subtlety in the code prior to the this commit
that caused UDPOR to incorrectly compute whether
or not `[e] + C` was a valid configuration. Specifically,
it was not sufficient to look at the difference between
the event's history and the events in the configuration
and checking *dependency*. You have to check *conflicts*:
it's possible that two events are dependent in a configuration
but are related to each other causally (and thus would
not be in conflict with one another)

13 months agoFix dynamic_cast<> typo for computation for CommRecv
Maxwell Pirtle [Tue, 4 Apr 2023 08:12:30 +0000 (10:12 +0200)]
Fix dynamic_cast<> typo for computation for CommRecv

There was a type check in the incremental computation
of extension sets for CommRecv that incorrectly cast
the value to a CommSend instead. I suppose this gave
us some undefined behavior as UDPOR correctly identified
the bug in some cases but not in other cases.
With the small fix, UDPOR now correctly identifies
the assertion failure in all cases in mc-failed-assertion.

13 months agoClarify that the issuer for a CommWait() action is that of the same actor
Maxwell Pirtle [Mon, 3 Apr 2023 09:42:38 +0000 (11:42 +0200)]
Clarify that the issuer for a CommWait() action is that of the same actor

The `CommWait()` transition, in the manner that SimGrid
handles communications, can be said to be "issued" by either
the sender or the receiver that are a part of the communication
under consideration. We favor that which is run by the same actor;
indeed, we require it as this point unless otherwise noted.

If it is possible for a `CommWait` to wait on a communication
whose identity cannot be traced back to an event that already
executed by the same actor, the model would have to change
when computing extension sets for CommWait(), specifically
when checking whether or not that transition is enabled
at a prior state

13 months agoAdd first round of debug logging to UDPOR
Maxwell Pirtle [Mon, 3 Apr 2023 08:18:31 +0000 (10:18 +0200)]
Add first round of debug logging to UDPOR

Several XBT_DEBUG() statements were added throughout
the functions in UdporChecker to better understand
the evolution of UDPOR in the context of SimGrid.
Several `to_string()` statements were added where
appropriate to aid in the visualization of the
unfolding structure. Until we potentially add
a more complicated tree-drawing algorithm to SimGrid
that can render the unfolding structure systematically,
this is the best we have

13 months agoIntermediate commit to prove that UDPOR functions
Maxwell Pirtle [Tue, 28 Mar 2023 11:44:12 +0000 (13:44 +0200)]
Intermediate commit to prove that UDPOR functions

This commit returns a const_cast<>-ed UnfoldingEvent
from the intersection of the sets A and ex(C) in
the Unfolding. We use this work around currently as
there is no way currently to distinguish between a
set of events and a set of constant events with
EventSet. To do so would require a number of changes
and probably a class that would be entirely duplicated
and more difficult to read without the help of e.g.
a template (which itself is not always the easiest to
read).

13 months agoFill in implementation of CommWait before large changes
Maxwell Pirtle [Mon, 27 Mar 2023 11:37:08 +0000 (13:37 +0200)]
Fill in implementation of CommWait before large changes

This commit adds the implementation of the extension
set computation before larger changes are added into
the UDPOR implementation.

What was discovered is that events hold stale references
to the transitions that they own. As UDPOR executes
actors in its quest to search the unfolding of the
application, the transitions that are executed are
potentially updated with additional information
*after* they have been executed. We'll need a way
to figure out how to manage this without causing an
absolute mess...

13 months agoAdd extension set computations without type casts
Maxwell Pirtle [Fri, 24 Mar 2023 13:08:41 +0000 (14:08 +0100)]
Add extension set computations without type casts

13 months agoAdd first steps for ex(C) for CommWait
Maxwell Pirtle [Fri, 24 Mar 2023 10:21:13 +0000 (11:21 +0100)]
Add first steps for ex(C) for CommWait

Computing the extension sets of a `CommWait`
action turns out to be a bit more involved than
I anticipated. In particular, we must determine
whether or not the transition is enabled at
some point in the past. This requires us to
find the event which created the communication
on which the `CommWait` waits and perform a
couple checks on that event. The current implementation
is not complete and is missing several important
steps, but it's a step in the right direction.

Additionally, some Sonar errors were fixed.

13 months agoMove state stack management to member on UnfoldingChecker
Maxwell Pirtle [Thu, 23 Mar 2023 08:19:08 +0000 (09:19 +0100)]
Move state stack management to member on UnfoldingChecker

Instead of passing around the variable `state_stack`
in a number of arguments in the UnfoldingChecker,
we moved the stack into a member on the class. This
also allows us to give a textual trace of what UDPOR
is searching much in the same way as is done with
DFSExplorer

13 months agoAdd comment on state restoration in UnfoldingChecker
Maxwell Pirtle [Wed, 22 Mar 2023 08:53:29 +0000 (09:53 +0100)]
Add comment on state restoration in UnfoldingChecker

13 months agoTrack the current sequence of states with UDPOR
Maxwell Pirtle [Wed, 22 Mar 2023 08:33:07 +0000 (09:33 +0100)]
Track the current sequence of states with UDPOR

Prior to this commit, we only tracked the "current"
state that was visited by the program. This is not
sufficient however: we must also keep track of the
sequence of states that UDPOR visited to *generate*
the configuration it is currently looking at. This
is required since we need to be able to generate
a fresh remote process when UDPOR decides to re-explore
a configuration `C` in its second recursive call
if it determines that an alternative exists. The
state regeneration is very similar (practically
identical) to that which is performed in the DFSChecker.

13 months agoReplace switch statement with map of handlers
Maxwell Pirtle [Wed, 22 Mar 2023 08:12:49 +0000 (09:12 +0100)]
Replace switch statement with map of handlers

13 months agoAdd skeleton implementation for ex(C) for CommSend
Maxwell Pirtle [Tue, 21 Mar 2023 09:13:42 +0000 (10:13 +0100)]
Add skeleton implementation for ex(C) for CommSend

13 months agoAdd skeleton implementations to ExtensionSetCalculator
Maxwell Pirtle [Mon, 20 Mar 2023 09:55:47 +0000 (10:55 +0100)]
Add skeleton implementations to ExtensionSetCalculator