diff --git a/src/hst/interleave.cc b/src/hst/interleave.cc index 533238b..2f31fd3 100644 --- a/src/hst/interleave.cc +++ b/src/hst/interleave.cc @@ -89,7 +89,8 @@ Interleave::initials(std::function op) const // ∪ (Ps = {STOP}? {✔}: {}) [rule 4] bool any_events = false; - for (const Process* p : ps_) { + for (const auto& process_and_count : ps_) { + const Process* p = process_and_count.first; p->initials([&any_events, &op](Event initial) { any_events = true; if (initial == Event::tick()) { @@ -119,9 +120,10 @@ Interleave::normal_afters(Event initial, // basic structure: Ps' = Ps ∖ {P} ∪ {P'}. Each Ps' starts with Ps, so go // ahead and add that to our Ps' set once. Process::Bag ps_prime(ps_); - for (const Process* p : ps_) { + for (const auto& process_and_count : ps_) { + const Process* p = process_and_count.first; // Set Ps' to Ps ∖ {P} - ps_prime.erase(ps_prime.find(p)); + ps_prime.erase(p); // Grab afters(P, a) p->afters(initial, [this, &op, &ps_prime](const Process& p_prime) { // ps_prime currently contains Ps. Add P' and remove P to produce @@ -130,7 +132,7 @@ Interleave::normal_afters(Event initial, // Create ⫴ (Ps ∖ {P} ∪ {P'}) as a result. op(*env_->interleave(ps_prime)); // Reset Ps' back to Ps ∖ {P}. - ps_prime.erase(ps_prime.find(&p_prime)); + ps_prime.erase(&p_prime); }); // Reset Ps' back to Ps. ps_prime.insert(p); @@ -153,7 +155,8 @@ Interleave::tau_afters(Event initial, // ahead and add that to our Ps' set once. Process::Bag ps_prime(ps_); // Find each P ∈ Ps where ✔ ∈ initials(P). - for (const Process* p : ps_) { + for (const auto& process_and_count : ps_) { + const Process* p = process_and_count.first; bool any_tick = false; p->initials([&any_tick](Event initial) { if (initial == Event::tick()) { @@ -162,11 +165,11 @@ Interleave::tau_afters(Event initial, }); if (any_tick) { // Create Ps ∖ {P} ∪ {STOP}) as a result. - ps_prime.erase(ps_prime.find(p)); + ps_prime.erase(p); ps_prime.insert(env_->stop()); op(*env_->interleave(ps_prime)); // Reset Ps' back to Ps. - ps_prime.erase(ps_prime.find(env_->stop())); + ps_prime.erase(env_->stop()); ps_prime.insert(p); } } @@ -177,7 +180,8 @@ Interleave::tick_afters(Event initial, std::function op) const { // afters(⫴ {STOP}, ✔) = {STOP} [rule 4] - for (const Process* p : ps_) { + for (const auto& process_and_count : ps_) { + const Process* p = process_and_count.first; bool any_events = false; p->initials([&any_events](Event _) { any_events = true; }); if (any_events) { @@ -204,8 +208,9 @@ Interleave::afters(Event initial, std::function op) const void Interleave::subprocesses(std::function op) const { - for (const Process* process : ps_) { - op(*process); + for (const auto& process_and_count : ps_) { + const Process* p = process_and_count.first; + op(*p); } } diff --git a/src/hst/process.cc b/src/hst/process.cc index 3a2fb65..f6ea406 100644 --- a/src/hst/process.cc +++ b/src/hst/process.cc @@ -8,6 +8,7 @@ #include "hst/process.h" #include +#include #include #include #include @@ -44,34 +45,57 @@ NormalizedProcess::afters(Event initial, } } +void +Process::Bag::insert(const Process* process) +{ + ++counts_[process]; +} + +void +Process::Bag::erase(const Process* process) +{ + auto it = counts_.find(process); + assert(it != counts_.end() && it->second != 0); + if (--it->second == 0) { + counts_.erase(it); + } +} + std::size_t Process::Bag::hash() const { static hash_scope scope; hst::hasher hash(scope); - std::vector sorted(begin(), end()); - std::sort(sorted.begin(), sorted.end()); - for (const Process* process : sorted) { + for (const Process* process : sorted()) { hash.add(*process); } return hash.value(); } -std::ostream& operator<<(std::ostream& out, const Process::Bag& processes) +std::vector +Process::Bag::sorted() const { - // We want reproducible output, so we sort the processes in the set before - // rendering them into the stream. We the process's index to print out the - // processes in the order that they were defined. - std::vector sorted_processes(processes.begin(), - processes.end()); - std::sort(sorted_processes.begin(), sorted_processes.end(), + std::vector sorted; + for (const auto& process_and_count : *this) { + const Process* process = process_and_count.first; + size_type count = process_and_count.second; + sorted.insert(sorted.end(), count, process); + } + std::sort(sorted.begin(), sorted.end(), [](const Process* p1, const Process* p2) { return p1->index() < p2->index(); }); + return sorted; +} +std::ostream& operator<<(std::ostream& out, const Process::Bag& processes) +{ + // We want reproducible output, so we sort the processes in the set before + // rendering them into the stream. We use the process's index as the sort + // key to print out the processes in the order that they were defined. bool first = true; out << "{"; - for (const Process* process : sorted_processes) { + for (const Process* process : processes.sorted()) { if (first) { first = false; } else { @@ -87,14 +111,23 @@ Process::Set::hash() const { static hash_scope scope; hst::hasher hash(scope); - std::vector sorted(begin(), end()); - std::sort(sorted.begin(), sorted.end()); - for (const Process* process : sorted) { + for (const Process* process : sorted()) { hash.add(*process); } return hash.value(); } +std::vector +Process::Set::sorted() const +{ + std::vector sorted(begin(), end()); + std::sort(sorted.begin(), sorted.end(), + [](const Process* p1, const Process* p2) { + return p1->index() < p2->index(); + }); + return sorted; +} + void Process::Set::tau_close() { @@ -118,16 +151,9 @@ std::ostream& operator<<(std::ostream& out, const Process::Set& processes) // We want reproducible output, so we sort the processes in the set before // rendering them into the stream. We the process's index to print out the // processes in the order that they were defined. - std::vector sorted_processes(processes.begin(), - processes.end()); - std::sort(sorted_processes.begin(), sorted_processes.end(), - [](const Process* p1, const Process* p2) { - return p1->index() < p2->index(); - }); - bool first = true; out << "{"; - for (const Process* process : sorted_processes) { + for (const Process* process : processes.sorted()) { if (first) { first = false; } else { diff --git a/src/hst/process.h b/src/hst/process.h index 3ebd6c5..65a34c5 100644 --- a/src/hst/process.h +++ b/src/hst/process.h @@ -11,9 +11,11 @@ #include #include #include +#include #include #include #include +#include #include #include @@ -123,14 +125,48 @@ class NormalizedProcess : public Process { void bfs(std::function op) const; }; -class Process::Bag : public std::unordered_multiset { +class Process::Bag { private: - using Parent = std::unordered_multiset; + using size_type = unsigned int; + using CountMap = std::unordered_map; public: - using Parent::unordered_multiset; + using const_iterator = CountMap::const_iterator; + using iterator = CountMap::iterator; + + Bag() = default; + Bag(const Bag& other) = default; + explicit Bag(std::initializer_list elements) + { + for (const Process* process : elements) { + insert(process); + } + } + + void insert(const Process* process); + + // Unlike the STL multimap classes, this only removes ONE copy of process. + void erase(const Process* process); std::size_t hash() const; + + // Returns a vector containing a sorted copy of the bag. Duplicate elements + // will be added to the vector multiple times. + std::vector sorted() const; + + bool operator==(const Bag& other) const { return counts_ == other.counts_; } + bool operator!=(const Bag& other) const { return counts_ != other.counts_; } + + // Returns an iterator of (Process, count) pairs + iterator begin() { return counts_.begin(); } + iterator end() { return counts_.end(); } + const_iterator begin() const { return counts_.begin(); } + const_iterator end() const { return counts_.end(); } + const_iterator cbegin() const { return counts_.begin(); } + const_iterator cend() const { return counts_.end(); } + + private: + CountMap counts_; }; std::ostream& operator<<(std::ostream& out, const Process::Bag& processes); @@ -144,6 +180,9 @@ class Process::Set : public std::unordered_set { std::size_t hash() const; + // Returns a vector containing a sorted copy of the set. + std::vector sorted() const; + // Updates this set of processes to be τ-closed. (That is, we add any // additional processes you can reach by following τ one or more times.) void tau_close(); @@ -271,12 +310,7 @@ Process::print_subprocesses(std::ostream& out, const T& processes, // We want reproducible output, so we sort the processes in the set before // rendering them into the stream. We the process's index to print out the // processes in the order that they were defined. - std::vector sorted_processes(processes.begin(), - processes.end()); - std::sort(sorted_processes.begin(), sorted_processes.end(), - [](const Process* p1, const Process* p2) { - return p1->index() < p2->index(); - }); + std::vector sorted_processes = processes.sorted(); if (sorted_processes.size() == 2) { const Process* lhs = sorted_processes[0];