Skip to content

Phase 3 of UDPOR Integration: Iteration Over Maximal Sets of a Configuration

Overview

This MR primarily introduces the maximal_subsets_iterator that can traverse the set of maximal subsets of events of the configuration that it traverses. The iterator gives you the option of filtering out events from consideration if they can be disqualified individually. This is useful e.g. when removing events whose associated transitions are not dependent with some transition t. This brings us a big step closer to computing the extension sets without special knowledge of each transition (which can be incrementally added in later with incrementally "minimal" effort).

Changes

  1. The most important changes are in maximal_subsets_iterator. This is an iterator that traverses what can be thought of as the graph of maximal events of the configuration. The problem can also be written/solved recursively, but providing an iterator gives us the benefit of all the C++ functions that operate on iterators. The implementation fortunately can simply build upon all of the constructs that existed prior to these changes; i.e. apart from the iterator itself, no new constructs were needed. I had some ideas of adding in e.g. a Causes struct that would encode which events some set of events causes and some extra iterators for traversing those causes; and while this would have worked perfectly well, it would have been a bunch of extra code that wouldn’t have ultimately been needed. If the need arises in the future to talk about causes, though, the appropriate changes can be made.

  2. Most references prior to this MR were to UnfoldingEvent*; but since mutation has not been needed, and likely will continue that way, most places now take in a const UnfoldingEvent*. All of the functionality/computation of UDPOR involves merely looking at events that already exist as opposed to modifying those events. It’s only at event-creation time during which e.g. an event’s causes need to be assigned, and events are removed entirely as opposed to partially (e.g. you’ll never remove only one immediate cause of an event).

  3. boost::iterator_facade<...> is now used with every iterator implementation thus far. It provides a simpler interface, removes a lot of code, and gives us full conformance to the specific iterator type (i.e. it catches edge cases that may be easy to miss on a first raw implementation of an iterator). The History::Iterator now benefits from boost::iterator_facade<...> as well.

What to Focus On

The primary focus should be on any subtitles you notice in any of the tests or the implementation of the maximal_subsets_iterator. The tests ironed out most of the initial unexpected behavior and I feel more confident in the "intuition" of each step of the algorithm than I had prior; but perhaps you can think of a case that should be accounted for.

Note: The maximal_subsets_iterator is a forward iterator only. There is likely a way to support backward iteration as well; for now, we support forward iteration only with most of the iterators that have been created until the need arises.

Future Changes

The roadmap is tentatively as follows:

  1. We need the ability to detect if two events are extensively equal (i.e. ==) rather than intensively equal (i.e. &a == &b). This requires us to check a) if an event's dependencies are equal and b) if the transitions associated with the event are run by the same actor at the same step. The same step bit is currently missing, and this will be investigated next.
  2. After computing ex(C), we need to compute en(C). This means determining conflicts among a set of events, which will be added in its own phase
  3. We need to compute K-partial alternatives. This is a relatively complex addition, so it will also come in its own phase
  4. "Finally", we need to compute the "clean-up" step of UDPOR and actually perform state regeneration as is done with the DFSExplorer. This step will probably build on a lot of what is added before

After these steps have been implemented, we should have an implementation of UDPOR sans specialized knowledge of each transition type. Subsequent phases will incrementally add the special conditions to improve the efficiency of computing ex(C) dramatically.

Merge request reports