Skip to content

Commit

Permalink
Merge pull request #29 from MortenSchou/solver-instance-json
Browse files Browse the repository at this point in the history 
Add JSON parser for Solver-Instance
  • Loading branch information
@MortenSchou
MortenSchou authored Mar 1, 2022
2 parents c9dfec1 + 0b6a1e5 commit 32a3fc9
Show file tree
Hide file tree
Showing 22 changed files with 2,217 additions and 641 deletions.
1 change: 1 addition & 0 deletions CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,7 @@ if(BUILD_TESTING AND PDAAAL_BuildTests)
add_test(NAME AutomatonPath_test COMMAND AutomatonPath_test)

if (PDAAAL_Build_Main) # We need the dependencies for pdaaal-bin to test it.
add_test(NAME Parser_test COMMAND Parser_test)
add_test(NAME Verification_test COMMAND Verification_test)
endif()

Expand Down
175 changes: 49 additions & 126 deletions src/include/pdaaal/PAutomaton.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ namespace pdaaal {
class PAutomaton : public internal::PAutomaton<W,trace_info_type>, private std::conditional_t<skip_state_mapping, no_state_mapping, state_mapping<state_t>> {
static_assert(!skip_state_mapping || std::is_same_v<state_t,size_t>, "When skip_state_mapping==true, you must use state_t=size_t");
using parent_t = internal::PAutomaton<W,trace_info_type>;
using parent2_t = std::conditional_t<skip_state_mapping, no_state_mapping, state_mapping<state_t>>;
using pda_t = PDA<label_t,W,fut::type::vector,state_t,skip_state_mapping>;
using internal_pda_t = typename pda_t::parent_t;
public:
Expand All @@ -60,6 +61,9 @@ namespace pdaaal {
PAutomaton(const pda_t& pda, const std::vector<size_t>& special_initial_states, bool special_accepting = true)
: parent_t(static_cast<const internal_pda_t&>(pda), special_initial_states, special_accepting), _pda(pda) { };

PAutomaton(PAutomaton<label_t,W,state_t,skip_state_mapping,trace_info_type>&& other, const pda_t& pda) noexcept // Move constructor, but update reference to PDA.
: parent_t(std::move(other), static_cast<const internal_pda_t&>(pda)), parent2_t(std::move(other)), _pda(pda) {};

[[nodiscard]] nlohmann::json to_json(const std::string& name = "P-automaton") const {
nlohmann::json j;
j[name] = *this;
Expand All @@ -84,20 +88,25 @@ namespace pdaaal {
}
size_t insert_state(const state_t& state) {
if constexpr (skip_state_mapping) {
return state; // + this->pda().states().size();
return state;
} else {
return this->_state_map.insert(state).second + _pda.states().size();
}
}

[[nodiscard]] state_t get_state(size_t id) const {
[[nodiscard]] std::optional<state_t> get_state_optional(size_t id) const {
if constexpr (skip_state_mapping) {
return id;
} else {
if (id < _pda.states().size()) {
return _pda.get_state(id);
} else {
return static_cast<const state_mapping<state_t>*>(this)->get_state(id - _pda.states().size());
auto offset = id - _pda.states().size();
if (offset < this->state_map_size()) {
return static_cast<const state_mapping<state_t>*>(this)->get_state(offset);
} else {
return std::nullopt;
}
}
}
}
Expand All @@ -114,142 +123,56 @@ namespace pdaaal {
template<typename label_t, typename W, typename state_t, bool skip_state_mapping, TraceInfoType trace_info_type = TraceInfoType::Single>
PAutomaton(const PDA<label_t,W,fut::type::vector,state_t,skip_state_mapping>&, const std::vector<size_t>&, bool special_accepting = true) -> PAutomaton<label_t,W,state_t,skip_state_mapping,trace_info_type>;

class PAutomatonJsonParser {
public:
template <TraceInfoType trace_info_type = TraceInfoType::Single, typename pda_t>
static auto parse(const std::string& file, pda_t& pda, const std::string& name = "P-automaton") {
std::ifstream file_stream(file);
if (!file_stream.is_open()) {
std::stringstream error;
error << "Could not open " << name << " file: " << file << std::endl;
throw std::runtime_error(error.str());
}
return parse<trace_info_type>(file_stream, pda, name);
}
template <TraceInfoType trace_info_type = TraceInfoType::Single, typename pda_t>
static auto parse(std::istream& istream, pda_t& pda, const std::string& name = "P-automaton") {
json j;
istream >> j;
return from_json<trace_info_type>(j[name], pda);
}
template <TraceInfoType trace_info_type, typename W>
static auto from_json(const json& j, PDA<std::string,W,fut::type::vector, std::string>& pda) {
return from_json<trace_info_type, std::string>(j, pda, [](const std::string& s) { return s; });
}
template <TraceInfoType trace_info_type, typename W, bool ssm>
static auto from_json(const json& j, PDA<std::string,W,fut::type::vector, size_t, ssm>& pda) {
return from_json<trace_info_type, size_t>(j, pda, [](const std::string& s) -> size_t { return std::stoul(s); });
}
private:
template <TraceInfoType trace_info_type, typename state_t, typename W, bool skip_state_mapping>
static auto from_json(const json& j,
PDA<std::string,W,fut::type::vector,state_t,skip_state_mapping>& pda,
const std::function<state_t(const std::string&)>& state_mapping) {
// TODO: Proper error checking and handling.!
auto iterate_states = [&j,&state_mapping](const std::function<void(const state_t&,const json&)>& fn) {
if constexpr (skip_state_mapping) {
assert(j["states"].is_array());
size_t i = 0;
for (const auto& j_state : j["states"]) {
fn(i, j_state);
++i;
}
} else {
assert(j["states"].is_object());
for (const auto& [name,j_state] : j["states"].items()) {
fn(state_mapping(name), j_state);
}
}
};
std::vector<size_t> accepting_initial_states;
std20::unordered_set<state_t> accepting_extra_states;
iterate_states([&pda,&accepting_initial_states,&accepting_extra_states](const state_t& state, const json& j_state){
auto [exists, id] = pda.exists_state(state);
if (exists) {
if (j_state.contains("accepting") && j_state["accepting"].get<bool>()) {
accepting_initial_states.emplace_back(id);
}
assert(j_state.contains("initial") && j_state["initial"].get<bool>());
} else {
if (j_state.contains("accepting") && j_state["accepting"].get<bool>()) {
accepting_extra_states.emplace(state);
}
assert(!(j_state.contains("initial") && j_state["initial"].get<bool>()));
}
});
std::sort(accepting_initial_states.begin(), accepting_initial_states.end());
accepting_initial_states.erase(std::unique(accepting_initial_states.begin(), accepting_initial_states.end()), accepting_initial_states.end());
PAutomaton<std::string, W, state_t, skip_state_mapping, trace_info_type> automaton(pda, accepting_initial_states, true);

auto state_to_id = [&automaton,&accepting_extra_states](const state_t& state){
auto [exists, id] = automaton.exists_state(state);
if (!exists) {
id = automaton.add_state(false, accepting_extra_states.contains(state));
auto id2 = automaton.insert_state(state);
assert(id == id2);
}
return id;
};

iterate_states([&state_to_id,&automaton,&state_mapping,&pda](const state_t& state, const json& j_state){
size_t from = state_to_id(state);
for (const auto& edge : j_state["edges"]) {
size_t to;
if constexpr (skip_state_mapping) {
assert(edge["to"].is_number_unsigned());
to = state_to_id(edge["to"].get<size_t>());
} else {
assert(edge["to"].is_string());
to = state_to_id(state_mapping(edge["to"].get<std::string>()));
}
auto label_string = edge["label"].get<std::string>();
if (label_string.empty()) {
automaton.add_epsilon_edge(from,to);
} else {
automaton.add_edge(from,to,pda.insert_label(label_string));
}
}
});
return automaton;
}
};
// Simplify type deduction elsewhere.
namespace details {
template<typename pda_t, TraceInfoType trace_info_type> struct pda_to_pautomaton;
template<typename label_t, typename W, typename state_t, bool skip_state_mapping, TraceInfoType trace_info_type>
struct pda_to_pautomaton<PDA<label_t,W,fut::type::vector,state_t,skip_state_mapping>, trace_info_type> {
using type = PAutomaton<label_t,W,state_t,skip_state_mapping,trace_info_type>;
};
}
template<typename pda_t, TraceInfoType trace_info_type = TraceInfoType::Single>
using pda_to_pautomaton_t = typename details::pda_to_pautomaton<pda_t,trace_info_type>::type;

template<typename label_t, typename W, typename state_t, bool skip_state_mapping, TraceInfoType trace_info_type>
void to_json(json& j, const PAutomaton<label_t,W,state_t,skip_state_mapping,trace_info_type>& automaton) {
template<bool with_initial = true, typename label_t, typename W, typename state_t, bool skip_state_mapping, TraceInfoType trace_info_type>
void to_json_impl(json& j, const PAutomaton<label_t,W,state_t,skip_state_mapping,trace_info_type>& automaton) {
j = json::object();
size_t num_pda_states = automaton.pda().states().size();
auto state_to_string = [&automaton](size_t state){
return details::label_to_string(automaton.get_state(state));
auto state_to_json_value = [&automaton](size_t state) -> json {
if constexpr(skip_state_mapping) {
return state;
} else {
if (auto s = automaton.get_state_optional(state); s) {
return details::label_to_string(s.value());
}
return state;
}
};
json j_states;
json j_edges = json::array();
for (const auto& state : automaton.states()) {
auto j_state = json::object();
if (state->_id < num_pda_states) {
j_state["initial"] = true;
auto j_from = state_to_json_value(state->_id);
if constexpr(with_initial) {
if (state->_id < num_pda_states) {
j["initial"].emplace_back(j_from);
}
}
if (state->_accepting) {
j_state["accepting"] = true;
j["accepting"].emplace_back(j_from);
}
j_state["edges"] = json::array();
for (const auto& [to, labels] : state->_edges) {
for (const auto& [label,tw] : labels) {
json edge;
if constexpr (skip_state_mapping) {
edge["to"] = to;
} else {
edge["to"] = state_to_string(to);
}
edge["label"] = label == automaton.epsilon ? "" : details::label_to_string(automaton.get_symbol(label));
j_state["edges"].emplace_back(edge);
j_edges.emplace_back(json::array(
{j_from,
label == automaton.epsilon ? "" : details::label_to_string(automaton.get_symbol(label)),
state_to_json_value(to)}));
}
}
if constexpr (skip_state_mapping) {
j_states.emplace_back(j_state);
} else {
j_states[state_to_string(state->_id)] = j_state;
}
}
j["states"] = j_states;
j["edges"] = j_edges;
}
template<typename label_t, typename W, typename state_t, bool skip_state_mapping, TraceInfoType trace_info_type>
void to_json(json& j, const PAutomaton<label_t,W,state_t,skip_state_mapping,trace_info_type>& automaton) {
to_json_impl(j,automaton);
}

}
Expand Down
28 changes: 28 additions & 0 deletions src/include/pdaaal/PAutomatonProduct.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,11 @@ namespace pdaaal {
_initial(std::move(initial), _pda), _final(std::move(final), _pda),
_product(_pda, get_initial_accepting(_initial, _final), true) {};

PAutomatonProduct(PAutomatonProduct&& other, const pda_t& pda) noexcept // Move constructor, but update reference to PDA.
: _pda(pda), _pda_size(_pda.states().size()), _initial(std::move(other._initial), _pda), _final(std::move(other._final), _pda),
_product(std::move(other._product), _pda), _swap_initial_final(other._swap_initial_final), _id_map(std::move(other._id_map)),
_id_fast_lookup(std::move(other._id_fast_lookup)), _id_fast_lookup_back(std::move(other._id_fast_lookup_back)) {};

// Returns whether an accepting state in the product automaton was reached.
template<bool needs_back_lookup = false, bool ET = true>
bool initialize_product() {
Expand Down Expand Up @@ -151,6 +156,12 @@ namespace pdaaal {
}
}

[[nodiscard]] nlohmann::json to_json() const {
nlohmann::json j;
j["instance"] = *this;
return j;
}

private:
template<bool edge_in_first = true, bool needs_back_lookup = false>
bool add_edge(size_t from, uint32_t label, size_t to, internal::edge_annotation_t<W> trace,
Expand Down Expand Up @@ -370,11 +381,28 @@ namespace pdaaal {
const NFA<label_t>& final_nfa, const std::vector<size_t>& final_states)
-> PAutomatonProduct<PDA<label_t,W,fut::type::vector,state_t,skip_state_mapping>,PAutomaton<label_t,W,state_t,skip_state_mapping,trace_info_type>,W>;

template<typename label_t, typename W, typename state_t, bool skip_state_mapping, TraceInfoType trace_info_type>
PAutomatonProduct(const PDA<label_t,W,fut::type::vector,state_t,skip_state_mapping>& pda,
PAutomaton<label_t,W,state_t,skip_state_mapping,trace_info_type>&& initial,
PAutomaton<label_t,W,state_t,skip_state_mapping,trace_info_type>&& final)
-> PAutomatonProduct<PDA<label_t,W,fut::type::vector,state_t,skip_state_mapping>,PAutomaton<label_t,W,state_t,skip_state_mapping,trace_info_type>,W,trace_info_type>;

template<typename label_t, typename W, typename state_t, bool skip_state_mapping, TraceInfoType trace_info_type>
PAutomatonProduct(const PDA<label_t,W,fut::type::vector,state_t,skip_state_mapping>& pda,
internal::PAutomaton<W,trace_info_type> initial, internal::PAutomaton<W,trace_info_type> final)
-> PAutomatonProduct<PDA<label_t,W,fut::type::vector,state_t,skip_state_mapping>,internal::PAutomaton<W,trace_info_type>,W,trace_info_type>;

template<typename label_t, typename W, fut::type Container, typename state_t, bool skip_state_mapping, TraceInfoType trace_info_type>
void to_json(json& j, const PAutomatonProduct<PDA<label_t,W,Container,state_t,skip_state_mapping>,PAutomaton<label_t,W,state_t,skip_state_mapping,trace_info_type>, W, trace_info_type>& instance) {
j = json::array();
j.emplace_back(json::object());
details::params_state_names(j.back(), instance.pda());
details::params_weight_type(j.back(), instance.pda());
j.emplace_back(instance.pda());
j.emplace_back(); to_json_impl<false>(j.back(),instance.initial_automaton()); // Don't print initial states in P-automata,
j.emplace_back(); to_json_impl<false>(j.back(),instance.final_automaton()); // since they are derived from the PDA.
}

}

#endif //PDAAAL_PAUTOMATONPRODUCT_H
48 changes: 48 additions & 0 deletions src/include/pdaaal/PDA.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,8 @@ namespace pdaaal {
class PDA : public internal::PDA<W, Container>, public std::conditional_t<skip_state_mapping, no_state_mapping, state_mapping<state_t>> {
public:
using parent_t = internal::PDA<W, Container>;
using expose_state_t = state_t; // Expose template parameter as dependent name.
static constexpr bool expose_skip_state_mapping = skip_state_mapping;
protected:
using impl_rule_t = typename internal::PDA<W, Container>::rule_t; // This rule type is used internally.
static_assert(!skip_state_mapping || std::is_same_v<state_t,size_t>, "When skip_state_mapping==true, you must use state_t=size_t");
Expand Down Expand Up @@ -383,6 +385,52 @@ namespace pdaaal {
j["states"] = j_states;
}

namespace details {
template<typename label_t, typename W>
void params_state_names(nlohmann::json& j, const PDA<label_t,W,fut::type::vector,size_t,true>&) {
j["state-names"] = false;
}
template<typename label_t, typename W, typename state_t>
void params_state_names(nlohmann::json& j, const PDA<label_t,W,fut::type::vector,state_t,false>&) {
j["state-names"] = true;
}
template<typename label_t, typename state_t, bool skip_state_mapping>
void params_weight_type(nlohmann::json& j, const PDA<label_t,weight<void>,fut::type::vector,state_t,skip_state_mapping>&) {
j["weight-type"] = "none";
}
template<typename Inner, std::size_t N, typename label_t, typename state_t, bool skip_state_mapping>
void params_weight_type(nlohmann::json& j, const PDA<label_t,weight<std::array<Inner,N>>,fut::type::vector,state_t,skip_state_mapping>&) {
static_assert(weight<std::array<Inner,N>>::is_weight);
j["weight-type"] = json::array();
if constexpr(weight<std::array<Inner,N>>::is_signed) {
j["weight-type"].emplace_back("int");
} else {
j["weight-type"].emplace_back("uint");
}
j["weight-type"].emplace_back(N);
}
template<typename Inner, typename label_t, typename state_t, bool skip_state_mapping>
void params_weight_type(nlohmann::json& j, const PDA<label_t,weight<std::vector<Inner>>,fut::type::vector,state_t,skip_state_mapping>&) {
static_assert(weight<std::vector<Inner>>::is_weight);
j["weight-type"] = json::array();
if constexpr(weight<std::vector<Inner>>::is_signed) {
j["weight-type"].emplace_back("int");
} else {
j["weight-type"].emplace_back("uint");
}
}
template<typename label_t, typename W, typename state_t, bool skip_state_mapping>
void params_weight_type(nlohmann::json& j, const PDA<label_t,W,fut::type::vector,state_t,skip_state_mapping>&) {
if constexpr(W::is_weight) {
if constexpr(W::is_signed) {
j["weight-type"] = "int";
} else {
j["weight-type"] = "uint";
}
}
}
}

}

#endif /* PDAAAL_PDA_H */
10 changes: 10 additions & 0 deletions src/include/pdaaal/SolverInstance.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,16 @@ namespace pdaaal {
SolverInstance(pda_t&& pda, pautomaton_t&& initial, pautomaton_t&& final)
: _pda(std::move(pda)), _product(_pda, std::move(initial), std::move(final)) {};

SolverInstance(SolverInstance&& other) noexcept
: _pda(std::move(other._pda)), _product(std::move(other._product), _pda) {};
SolverInstance& operator=(SolverInstance&& other) noexcept {
if (this != &other) {
_pda = std::move(other._pda);
_product = product_t(std::move(other._product), _pda);
}
return *this;
}

product_t* operator->() {
return &_product;
}
Expand Down
Loading

0 comments on commit 32a3fc9

Please sign in to comment.