Commit 6a57597a authored by Andrew Cornell's avatar Andrew Cornell
Browse files

Fully working commit

parents
# .build folder
.build/
# VSCode config
.vscode
# Analysis files
analysis/
# macOS Finder
.DS_Store
\ No newline at end of file
# CMake script for nfa-prune
cmake_minimum_required(VERSION 3.10)
project(nfa_prune
LANGUAGES CXX)
# Include cmake helpers
include(GNUInstallDirs)
# Find dependencies
find_package(boost REQUIRED)
# Set up target
add_executable(nfa_prune
"src/main.cpp"
"src/NFA.cpp"
"src/Delegator.cpp")
# Configure target: Compilation features
target_compile_features(nfa_prune PUBLIC cxx_std_17)
# Configure target: Set up dependencies
target_link_libraries(nfa_prune
PUBLIC
Boost::boost
"/usr/local/opt/llvm/lib/libc++fs.a")
# Configure installation
install(TARGETS nfa_prune
EXPORT nfa_prune
ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR}
LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR}
RUNTIME DESTINATION ${CMAKE_INSTALL_BINDIR})
\ No newline at end of file
// Delegator.cpp
// ============================================================================================
/// Implements the non-template symbols of `delegator.hpp`
#include "Delegator.hpp"
#include <stack>
#include <queue>
#include "DelegatorGame.hpp"
#include "PositionMap.hpp"
namespace {
using namespace delegator;
/// The state of a position in the top-down algorithm
enum class PositionState {
None,
Looping,
Unsafe,
Safe
};
/// Data attached to positions in the delegator game in the top-down algorithm
struct PositionData {
PositionState state;
bool active;
std::size_t count;
};
/// `Check` procedure from the top-down algorithm
auto check(NFA const& automaton, Position pos, PositionMap<PositionData>& data) -> PositionState;
/// `CheckPlayer0` procedure from the top-down algorithm
auto checkPlayer0(NFA const& automaton, std::size_t a, std::size_t q, std::size_t p, PositionMap<PositionData>& data) -> void;
/// `CheckPlayer1` procedure from the top-down algorithm
auto checkPlayer1(NFA const& automaton, std::size_t a, std::size_t q, std::size_t p, PositionMap<PositionData>& data) -> void;
/// `PropagateUnsafePlayer0` procedure from the top-down algorithm
auto propagateUnsafePlayer0(NFA const& automaton, std::size_t a, std::size_t q, std::size_t p, PositionMap<PositionData>& data) -> void;
/// `PropagateUnsafePlayer1` procedure from the top-down algorithm
auto propagateUnsafePlayer1(NFA const& automaton, std::size_t a, std::size_t q, std::size_t p, PositionMap<PositionData>& data) -> void;
/// Computes the share of visited vertices in a run of the top-down algorithm
auto computeLoad_TopDown(PositionMap<PositionData> const& data, NFA const& automaton) -> double;
/// Computes the share of visited vertices in a run of the bottom-up algorithm
auto computeLoad_BottomUp(PositionMap<std::size_t> const& count, NFA const& automaton) -> double;
auto check(NFA const& automaton, Position pos, PositionMap<PositionData>& data) -> PositionState {
if (data(pos).active) {
data(pos).state = PositionState::Looping;
}
else if (data(pos).state == PositionState::None) {
data(pos).active = true;
if (pos.player == Player::Player0) {
checkPlayer0(automaton, pos.lookahead, pos.state1, pos.state2, data);
}
else {
checkPlayer1(automaton, pos.lookahead, pos.state1, pos.state2, data);
}
data(pos).active = false;
}
return data(pos).state;
}
auto checkPlayer0(NFA const& automaton, std::size_t a, std::size_t q, std::size_t p, PositionMap<PositionData>& data) -> void {
auto& current_data = data(Player::Player0, a, q, p);
if (automaton.states[q].out_transitions[a].targets.size() == 0) {
current_data.state = PositionState::Safe;
return;
}
for (std::size_t q_prime: automaton.states[q].out_transitions[a].targets) {
if (check(automaton, { Player::Player1, a, q_prime, p }, data) == PositionState::Safe) {
current_data.state = PositionState::Safe;
return;
}
}
for (std::size_t q_prime: automaton.states[q].out_transitions[a].targets) {
if (data(Player::Player1, a, q_prime, p).state == PositionState::Looping) {
++current_data.count;
}
}
if (current_data.count == 0) {
if (current_data.state == PositionState::Looping) {
propagateUnsafePlayer0(automaton, a, q, p, data);
}
current_data.state = PositionState::Unsafe;
}
else {
current_data.state = PositionState::Looping;
}
}
auto checkPlayer1(NFA const& automaton, std::size_t a, std::size_t q, std::size_t p, PositionMap<PositionData>& data) -> void {
auto& current_data = data(Player::Player1, a, q, p);
if (!automaton.states[q].accepting) {
for (auto p_prime: automaton.states[p].out_transitions[a].targets) {
if (automaton.states[p_prime].accepting) {
current_data.state = PositionState::Unsafe;
return;
}
}
}
for (std::size_t b = 0; b != automaton.alphabetSize; ++b) {
for (auto p_prime: automaton.states[p].out_transitions[a].targets) {
if (check(automaton, { Player::Player0, b, q, p_prime }, data) == PositionState::Unsafe) {
if (current_data.state == PositionState::Looping) {
propagateUnsafePlayer1(automaton, a, q, p, data);
}
current_data.state = PositionState::Unsafe;
return;
}
}
}
for (std::size_t b = 0; b != automaton.alphabetSize; ++b) {
for (auto p_prime: automaton.states[p].out_transitions[a].targets) {
if (data(Player::Player0, b, q, p_prime).state == PositionState::Looping) {
current_data.count = 1;
current_data.state = PositionState::Looping;
return;
}
}
}
current_data.state = PositionState::Safe;
}
auto propagateUnsafePlayer0(NFA const& automaton, std::size_t a, std::size_t q, std::size_t p, PositionMap<PositionData>& data) -> void {
for (std::size_t b = 0; b != automaton.alphabetSize; ++b) {
for (auto p_prime: automaton.states[p].in_transitions[b].targets) {
auto& current_data = data(Player::Player1, b, q, p_prime);
if (current_data.count != 0) {
--current_data.count;
if (current_data.count == 0) {
propagateUnsafePlayer1(automaton, b, q, p_prime, data);
current_data.state = PositionState::Unsafe;
}
}
}
}
}
auto propagateUnsafePlayer1(NFA const& automaton, std::size_t a, std::size_t q, std::size_t p, PositionMap<PositionData>& data) -> void {
for (auto q_prime: automaton.states[q].in_transitions[a].targets) {
auto& current_data = data(Player::Player0, a, q_prime, p);
if (current_data.count != 0) {
--current_data.count;
if (current_data.count == 0) {
propagateUnsafePlayer0(automaton, a, q_prime, p, data);
current_data.state = PositionState::Unsafe;
}
}
}
}
auto computeLoad_TopDown(PositionMap<PositionData> const& data, NFA const& automaton) -> double {
auto load = 0.0;
for (std::size_t q = 0; q != automaton.states.size(); ++q) {
for (std::size_t p = 0; p != automaton.states.size(); ++p) {
for (std::size_t a = 0; a != automaton.alphabetSize; ++a) {
if (data(Player::Player0, a, q, p).state != PositionState::None) {
++load;
}
if (data(Player::Player1, a, q, p).state != PositionState::None) {
++load;
}
}
}
}
load /= (2 * automaton.states.size() * automaton.states.size() * automaton.alphabetSize);
return load;
}
auto computeLoad_BottomUp(PositionMap<std::size_t> const& count, NFA const& automaton) -> double {
auto load = 0.0;
for (std::size_t q = 0; q != automaton.states.size(); ++q) {
for (std::size_t p = 0; p != automaton.states.size(); ++p) {
for (std::size_t a = 0; a != automaton.alphabetSize; ++a) {
if (count(Player::Player0, a, q, p) != automaton.states[q].out_transitions[a].targets.size()) {
++load;
}
if (count(Player::Player1, a, q, p) != 1) {
++load;
}
}
}
}
load /= (2 * automaton.states.size() * automaton.states.size() * automaton.alphabetSize);
return load;
}
}
delegator::Delegator::Delegator(std::size_t states, std::size_t alphabet): _map(states * alphabet), _alphabet(alphabet) {
}
delegator::Delegator::Delegator(NFA const& automaton): _map(automaton.states.size() * automaton.alphabetSize), _alphabet(automaton.alphabetSize) {
}
auto delegator::Delegator::operator()(std::size_t q, std::size_t a) -> std::size_t& {
return _map[q * _alphabet + a];
}
auto delegator::Delegator::operator()(std::size_t q, std::size_t a) const -> std::size_t const& {
return _map[q * _alphabet + a];
}
auto delegator::topDown(NFA const& automaton, double* load) -> std::optional<Delegator> {
PositionMap<PositionData> data(automaton);
for (std::size_t q = 0; q != automaton.states.size(); ++q) {
for (std::size_t p = 0; p != automaton.states.size(); ++p) {
for (std::size_t a = 0; a != automaton.alphabetSize; ++a) {
data(Player::Player0, a, q, p) = { PositionState::None, false, 0 };
data(Player::Player1, a, q, p) = { PositionState::None, false, 0 };
}
}
}
for (std::size_t a = 0; a != automaton.alphabetSize; ++a) {
if (check(automaton, { Player::Player0, a, 0, 0 }, data) == PositionState::Unsafe) {
if (load) {
*load = computeLoad_TopDown(data, automaton);
}
return std::nullopt;
}
}
Delegator f(automaton);
for (std::size_t q = 0; q != automaton.states.size(); ++q) {
for (std::size_t a = 0; a != automaton.alphabetSize; ++a) {
for (std::size_t q_prime = 0; q_prime != automaton.states.size(); ++q_prime) {
if (automaton.states[q].out_transitions[a].targets.count(q_prime)) {
if (data(Player::Player1, a, q_prime, q).state != PositionState::Unsafe) {
f(q, a) = q_prime;
break;
}
}
}
}
}
if (load) {
*load = computeLoad_TopDown(data, automaton);
}
return f;
}
auto delegator::bottomUpQueue(NFA const& automaton, double* load) -> std::optional<Delegator> {
std::queue<Position> queue;
PositionMap<std::size_t> count(automaton);
for (std::size_t q = 0; q != automaton.states.size(); ++q) {
auto q_state = automaton.states[q];
for (std::size_t p = 0; p != automaton.states.size(); ++p) {
auto p_state = automaton.states[p];
if (!q_state.accepting && p_state.accepting) {
queue.push({ Player::Player0, automaton.alphabetSize, q, p });
}
for (std::size_t a = 0; a != automaton.alphabetSize; ++a) {
count(Player::Player0, a, q, p) = q_state.out_transitions[a].targets.size();
count(Player::Player1, a, q, p) = 1;
}
}
}
while (!queue.empty()) {
auto [i, a, q, p] = queue.front();
queue.pop();
if (i == Player::Player0) {
for (std::size_t b = 0; b != automaton.alphabetSize; ++b) {
for (auto p_prime: automaton.states[p].in_transitions[b].targets) {
if (count(Player::Player1, b, q, p_prime) == 0) {
continue;
}
--count(Player::Player1, b, q, p_prime);
if (count(Player::Player1, b, q, p_prime) == 0) {
queue.push({ Player::Player1, b, q, p_prime });
}
}
}
}
else {
for (std::size_t q_prime: automaton.states[q].in_transitions[a].targets) {
if (count(Player::Player0, a, q_prime, p) == 0) {
continue;
}
--count(Player::Player0, a, q_prime, p);
if (count(Player::Player0, a, q_prime, p) == 0) {
if (q_prime == 0 && p == 0) {
if (load) {
*load = computeLoad_BottomUp(count, automaton);
}
return std::nullopt;
}
else {
queue.push({ Player::Player0, a, q_prime, p });
}
}
}
}
}
Delegator f(automaton);
for (std::size_t q = 0; q != automaton.states.size(); ++q) {
for (std::size_t a = 0; a != automaton.alphabetSize; ++a) {
for (std::size_t q_prime = 0; q_prime != automaton.states.size(); ++q_prime) {
if (automaton.states[q].out_transitions[a].targets.count(q_prime)) {
if (count(Player::Player1, a, q_prime, q) != 0) {
f(q, a) = q_prime;
break;
}
}
}
}
}
if (load) {
*load = computeLoad_BottomUp(count, automaton);
}
return f;
}
auto delegator::bottomUpStack(NFA const& automaton, double* load) -> std::optional<Delegator> {
std::stack<Position> stack;
PositionMap<std::size_t> count(automaton);
for (std::size_t q = 0; q != automaton.states.size(); ++q) {
auto q_state = automaton.states[q];
for (std::size_t p = 0; p != automaton.states.size(); ++p) {
auto p_state = automaton.states[p];
if (!q_state.accepting && p_state.accepting) {
stack.push({ Player::Player0, automaton.alphabetSize, q, p });
}
for (std::size_t a = 0; a != automaton.alphabetSize; ++a) {
count(Player::Player0, a, q, p) = q_state.out_transitions[a].targets.size();
count(Player::Player1, a, q, p) = 1;
}
}
}
while (!stack.empty()) {
auto [i, a, q, p] = stack.top();
stack.pop();
if (i == Player::Player0) {
for (std::size_t b = 0; b != automaton.alphabetSize; ++b) {
for (auto p_prime: automaton.states[p].in_transitions[b].targets) {
if (count(Player::Player1, b, q, p_prime) == 0) {
continue;
}
--count(Player::Player1, b, q, p_prime);
if (count(Player::Player1, b, q, p_prime) == 0) {
stack.push({ Player::Player1, b, q, p_prime });
}
}
}
}
else {
for (std::size_t q_prime: automaton.states[q].in_transitions[a].targets) {
if (count(Player::Player0, a, q_prime, p) == 0) {
continue;
}
--count(Player::Player0, a, q_prime, p);
if (count(Player::Player0, a, q_prime, p) == 0) {
if (q_prime == 0 && p == 0) {
if (load) {
*load = computeLoad_BottomUp(count, automaton);
}
return std::nullopt;
}
else {
stack.push({ Player::Player0, a, q_prime, p });
}
}
}
}
}
Delegator f(automaton);
for (std::size_t q = 0; q != automaton.states.size(); ++q) {
for (std::size_t a = 0; a != automaton.alphabetSize; ++a) {
for (std::size_t q_prime = 0; q_prime != automaton.states.size(); ++q_prime) {
if (automaton.states[q].out_transitions[a].targets.count(q_prime)) {
if (count(Player::Player1, a, q_prime, q) != 0) {
f(q, a) = q_prime;
break;
}
}
}
}
}
if (load) {
*load = computeLoad_BottomUp(count, automaton);
}
return f;
}
\ No newline at end of file
// Delegator.hpp
// ============================================================================================
/// Contains a class representing a _k_-lookahead delegator
#ifndef DELEGATOR_AUTOMATA_DELEGATOR_HPP_INCLUDED
#define DELEGATOR_AUTOMATA_DELEGATOR_HPP_INCLUDED
#include <optional>
#include <vector>
#include "NFA.hpp"
namespace delegator {
/// Represents a 0-lookahead delegator for an NFA
///
/// First dimension is the source state, second dimension is the letter
class Delegator {
/// Map between pairs of state and letter to state (the delegator function)
///
/// First dimension: State
/// Second dimension: Letter
std::vector<std::size_t> _map;
/// The size of the alphabet of the automaton of the delegator
std::size_t _alphabet;
public:
/// Creates a new delegator function
///
/// \param states The number of states of the automaton of the delegator function
/// \param alphabet The size of the alphabet of the automaton of the delegator function
Delegator(std::size_t states, std::size_t alphabet);
/// Creates a new delegator function
///
/// \param automaton The automaton of the delegator function
Delegator(NFA const& automaton);
/// Gets the result of the delegator for a state-letter pair
///
/// \param q The state
/// \param a The letter
/// \returns The result of the delegator
auto operator()(std::size_t q, std::size_t a) -> std::size_t&;
/// Gets the result of the delegator for a state-letter pair
///
/// \param q The state
/// \param a The letter
/// \returns The result of the delegator
auto operator()(std::size_t q, std::size_t a) const -> std::size_t const&;
};
/// Tries to determine a delegator for an NFA using the top-down algorithm
///
/// \param automaton The automaton for which a delegator should be determined
/// \param load If not `null` will contain the fraction of game positions actually seen by the algorithm
/// \returns The delegator for `automaton` if one exists
auto topDown(NFA const& automaton, double* load = nullptr) -> std::optional<Delegator>;
/// Tries to determine a delegator for an NFA using the bottom-up algorithm using a stack
///
/// \param automaton The automaton for which a delegator should be determined
/// \param load If not `null` will contain the fraction of game positions actually seen by the algorithm
/// \returns The delegator for `automaton` if one exists
auto bottomUpStack(NFA const& automaton, double* load = nullptr) -> std::optional<Delegator>;
/// Tries to determine a delegator for an NFA using the bottom-up algorithm using a queue
///
/// \param automaton The automaton for which a delegator should be determined
/// \param load If not `null` will contain the fraction of game positions actually seen by the algorithm
/// \returns The delegator for `automaton` if one exists
auto bottomUpQueue(NFA const& automaton, double* load = nullptr) -> std::optional<Delegator>;
}
#endif /* DELEGATOR_AUTOMATA_DELEGATOR_HPP_INCLUDED */
// DelegatorGame.hpp
// ============================================================================================
/// Contains definitions for the delegator safety game
#ifndef DELEGATOR_DELEGATORGAME_HPP_INCLUDED
#define DELEGATOR_DELEGATORGAME_HPP_INCLUDED
#include <cstddef>
namespace delegator {
/// A player of a safety game
enum class Player {
/// Player 0
Player0 = 0,
/// Player 1
Player1 = 1
};
/// A position in a delegator safety game
struct Position final {
/// The player this position belongs to
Player player;
/// The lookahead at the position (= alphabet for empty lookahead)
std::size_t lookahead;
/// The state for player 0
std::size_t state1;
/// The state for player 1
std::size_t state2;
};
}
#endif /* DELEGATOR_DELEGATORGAME_HPP_INCLUDED */
\ No newline at end of file
// Metrics.hpp
// ============================================================================================
/// Contains methods for measuring runtime of methods
#ifndef DELEGATOR_METRICS_HPP_INCLUDED
#define DELEGATOR_METRICS_HPP_INCLUDED
#include <chrono>
#include <utility>
#include <tuple>
namespace delegator {
/// Measures the running time of a function
///
/// \tparam Clock The clock that should be used to measure the running time
/// \tparam Function The type of the function that should be measured
/// \tparam Args A template parameter pack of the argument types with which `func` should be invoked
/// \param func The function whose running time should be measured
/// \param args The parameters with which `func` should be invoked
/// \return The running time of `func` invoked with `args` measured with `Clock`
template <typename Clock, typename Function, typename... Args>
auto measure(Function func, Args&&... args) -> std::tuple<std::invoke_result_t<Function, Args...>, typename Clock::duration>;
}
// Template implementations