diff --git a/resources/examples/testfiles/lab/nondet.choicelab b/resources/examples/testfiles/lab/nondet.choicelab new file mode 100644 index 000000000..066f9fd21 --- /dev/null +++ b/resources/examples/testfiles/lab/nondet.choicelab @@ -0,0 +1,8 @@ +#DECLARATION +alpha beta gamma delta +#END +0 0 alpha +0 1 alpha beta +0 2 gamma +1 0 beta +3 2 beta \ No newline at end of file diff --git a/src/storm/models/sparse/ChoiceLabeling.cpp b/src/storm/models/sparse/ChoiceLabeling.cpp index 5e3c90904..6c12d3a73 100644 --- a/src/storm/models/sparse/ChoiceLabeling.cpp +++ b/src/storm/models/sparse/ChoiceLabeling.cpp @@ -1,4 +1,4 @@ -#include "ChoiceLabeling.h" +#include "storm/models/sparse/ChoiceLabeling.h" @@ -21,7 +21,10 @@ namespace storm { // Intentionally left empty. } - + bool ChoiceLabeling::isChoiceLabeling() const { + return true; + } + bool ChoiceLabeling::operator==(ChoiceLabeling const& other) const { if (itemCount != other.itemCount) { return false; @@ -40,14 +43,10 @@ namespace storm { return true; } - - ChoiceLabeling ChoiceLabeling::getSubLabeling(storm::storage::BitVector const& choices) const { return ChoiceLabeling(ItemLabeling::getSubLabeling(choices)); } - - std::set ChoiceLabeling::getLabelsOfChoice(uint64_t choice) const { return this->getLabelsOfItem(choice); } diff --git a/src/storm/models/sparse/ChoiceLabeling.h b/src/storm/models/sparse/ChoiceLabeling.h index 880133ee1..61403fa91 100644 --- a/src/storm/models/sparse/ChoiceLabeling.h +++ b/src/storm/models/sparse/ChoiceLabeling.h @@ -24,7 +24,8 @@ namespace storm { ChoiceLabeling(ItemLabeling const&& other); ChoiceLabeling& operator=(ChoiceLabeling const& other) = default; - + virtual bool isChoiceLabeling() const override ; + /*! * Checks whether the two labelings are equal. * diff --git a/src/storm/models/sparse/ItemLabeling.cpp b/src/storm/models/sparse/ItemLabeling.cpp index eba424a70..17a58ec44 100644 --- a/src/storm/models/sparse/ItemLabeling.cpp +++ b/src/storm/models/sparse/ItemLabeling.cpp @@ -1,5 +1,8 @@ #include "storm/models/sparse/ItemLabeling.h" +#include "storm/models/sparse/StateLabeling.h" +#include "storm/models/sparse/ChoiceLabeling.h" + #include "storm/exceptions/OutOfRangeException.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -11,6 +14,26 @@ namespace storm { // Intentionally left empty. } + bool ItemLabeling::isStateLabeling() const { + return false; + } + bool ItemLabeling::isChoiceLabeling() const { + return false; + } + + StateLabeling const& ItemLabeling::asStateLabeling() const { + return dynamic_cast(*this); + } + StateLabeling& ItemLabeling::asStateLabeling() { + return dynamic_cast(*this); + } + ChoiceLabeling const& ItemLabeling::asChoiceLabeling() const { + return dynamic_cast(*this); + } + ChoiceLabeling& ItemLabeling::asChoiceLabeling() { + return dynamic_cast(*this); + } + bool ItemLabeling::operator==(ItemLabeling const& other) const { if (itemCount != other.itemCount) { return false; diff --git a/src/storm/models/sparse/ItemLabeling.h b/src/storm/models/sparse/ItemLabeling.h index fb39f4433..14e752031 100644 --- a/src/storm/models/sparse/ItemLabeling.h +++ b/src/storm/models/sparse/ItemLabeling.h @@ -15,6 +15,9 @@ namespace storm { namespace models { namespace sparse { + class StateLabeling; + class ChoiceLabeling; + /*! * A base class managing the labeling of items with a number of (atomic) labels. */ @@ -31,6 +34,14 @@ namespace storm { ItemLabeling& operator=(ItemLabeling const& other) = default; + virtual bool isStateLabeling() const; + virtual bool isChoiceLabeling() const; + + StateLabeling const& asStateLabeling() const; + StateLabeling& asStateLabeling(); + ChoiceLabeling const& asChoiceLabeling() const; + ChoiceLabeling& asChoiceLabeling(); + /*! * Checks whether the two labelings are equal. * diff --git a/src/storm/models/sparse/StateLabeling.cpp b/src/storm/models/sparse/StateLabeling.cpp index ef0315669..e80556108 100644 --- a/src/storm/models/sparse/StateLabeling.cpp +++ b/src/storm/models/sparse/StateLabeling.cpp @@ -19,6 +19,10 @@ namespace storm { // Intentionally left empty. } + bool StateLabeling::isStateLabeling() const { + return true; + } + bool StateLabeling::operator==(StateLabeling const& other) const { if (itemCount != other.itemCount) { return false; diff --git a/src/storm/models/sparse/StateLabeling.h b/src/storm/models/sparse/StateLabeling.h index 4639b108e..99afcc80d 100644 --- a/src/storm/models/sparse/StateLabeling.h +++ b/src/storm/models/sparse/StateLabeling.h @@ -32,6 +32,7 @@ namespace storm { StateLabeling(ItemLabeling const&& other); StateLabeling& operator=(StateLabeling const& other) = default; + virtual bool isStateLabeling() const override; /*! * Checks whether the two labelings are equal. diff --git a/src/storm/parser/AutoParser.cpp b/src/storm/parser/AutoParser.cpp index 9d3069738..e277a7f1d 100644 --- a/src/storm/parser/AutoParser.cpp +++ b/src/storm/parser/AutoParser.cpp @@ -35,12 +35,12 @@ namespace storm { switch (type) { case storm::models::ModelType::Dtmc: { - model = std::shared_ptr>>(new storm::models::sparse::Dtmc>(std::move(DeterministicModelParser::parseDtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); + model = std::shared_ptr>>(new storm::models::sparse::Dtmc>(std::move(DeterministicModelParser::parseDtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename)))); break; } case storm::models::ModelType::Ctmc: { - model = std::shared_ptr>>(new storm::models::sparse::Ctmc>(std::move(DeterministicModelParser::parseCtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); + model = std::shared_ptr>>(new storm::models::sparse::Ctmc>(std::move(DeterministicModelParser::parseCtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename)))); break; } case storm::models::ModelType::Mdp: @@ -50,7 +50,7 @@ namespace storm { } case storm::models::ModelType::MarkovAutomaton: { - model = std::shared_ptr>>(new storm::models::sparse::MarkovAutomaton>(std::move(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); + model = std::shared_ptr>>(new storm::models::sparse::MarkovAutomaton>(std::move(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename)))); break; } default: diff --git a/src/storm/parser/DeterministicModelParser.cpp b/src/storm/parser/DeterministicModelParser.cpp index 9976e67dc..f6cf0180e 100644 --- a/src/storm/parser/DeterministicModelParser.cpp +++ b/src/storm/parser/DeterministicModelParser.cpp @@ -6,7 +6,7 @@ #include "storm/models/sparse/StandardRewardModel.h" #include "storm/parser/DeterministicSparseTransitionParser.h" -#include "storm/parser/AtomicPropositionLabelingParser.h" +#include "storm/parser/SparseItemLabelingParser.h" #include "storm/parser/SparseStateRewardParser.h" #include "storm/adapters/CarlAdapter.h" @@ -15,7 +15,7 @@ namespace storm { namespace parser { template - typename DeterministicModelParser::Result DeterministicModelParser::parseDeterministicModel(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename) { + typename DeterministicModelParser::Result DeterministicModelParser::parseDeterministicModel(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename, std::string const& choiceLabelingFilename) { // Parse the transitions. storm::storage::SparseMatrix transitions(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(transitionsFilename))); @@ -23,7 +23,7 @@ namespace storm { uint_fast64_t stateCount = transitions.getColumnCount(); // Parse the state labeling. - storm::models::sparse::StateLabeling labeling(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename)); + storm::models::sparse::StateLabeling labeling(storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename)); // Construct the result. DeterministicModelParser::Result result(std::move(transitions), std::move(labeling)); @@ -37,30 +37,36 @@ namespace storm { if (transitionRewardFilename != "") { result.transitionRewards = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(transitionRewardFilename, result.transitionSystem); } + + // Only parse choice labeling if a file is given. + boost::optional choiceLabeling; + if (!choiceLabelingFilename.empty()) { + result.choiceLabeling = storm::parser::SparseItemLabelingParser::parseChoiceLabeling(result.transitionSystem.getRowCount(), choiceLabelingFilename); + } return result; } template - storm::models::sparse::Dtmc> DeterministicModelParser::parseDtmc(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename) { - typename DeterministicModelParser::Result parserResult(std::move(parseDeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))); + storm::models::sparse::Dtmc> DeterministicModelParser::parseDtmc(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename, std::string const& choiceLabelingFilename) { + typename DeterministicModelParser::Result parserResult(std::move(parseDeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename))); std::unordered_map> rewardModels; if (!stateRewardFilename.empty() || !transitionRewardFilename.empty()) { rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(parserResult.stateRewards, boost::optional>(), parserResult.transitionRewards))); } - return storm::models::sparse::Dtmc>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(rewardModels)); + return storm::models::sparse::Dtmc>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(rewardModels), std::move(parserResult.choiceLabeling)); } template - storm::models::sparse::Ctmc> DeterministicModelParser::parseCtmc(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename) { - typename DeterministicModelParser::Result parserResult(std::move(parseDeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))); + storm::models::sparse::Ctmc> DeterministicModelParser::parseCtmc(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename, std::string const& choiceLabelingFilename) { + typename DeterministicModelParser::Result parserResult(std::move(parseDeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename))); std::unordered_map> rewardModels; if (!stateRewardFilename.empty() || !transitionRewardFilename.empty()) { rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(parserResult.stateRewards, boost::optional>(), parserResult.transitionRewards))); } - return storm::models::sparse::Ctmc>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(rewardModels), boost::none); + return storm::models::sparse::Ctmc>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(rewardModels), std::move(parserResult.choiceLabeling)); } template class DeterministicModelParser; diff --git a/src/storm/parser/DeterministicModelParser.h b/src/storm/parser/DeterministicModelParser.h index c247b2389..a30ef6d3c 100644 --- a/src/storm/parser/DeterministicModelParser.h +++ b/src/storm/parser/DeterministicModelParser.h @@ -53,6 +53,9 @@ namespace storm { //! Optional rewards for each transition. boost::optional> transitionRewards; + + //! The labels of each choice. + boost::optional choiceLabeling; }; @@ -69,12 +72,14 @@ namespace storm { * @param labelingFilename The path and name of the file containing the labels for the states of the model. * @param stateRewardFilename The path and name of the file containing the state reward of the model. This file is optional. * @param transitionRewardFilename The path and name of the file containing the transition rewards of the model. This file is optional. + * @param choiceLabelingFilename The path and name of the file containing the choice labeling of the model. This file is optional. * @return The parsed Dtmc. */ static storm::models::sparse::Dtmc> parseDtmc(std::string const& transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename = "", - std::string const & transitionRewardFilename = ""); + std::string const & transitionRewardFilename = "", + std::string const & choiceLabelingFilename = ""); /*! * Parse a Ctmc. @@ -89,12 +94,16 @@ namespace storm { * @param labelingFilename The path and name of the file containing the labels for the states of the model. * @param stateRewardFilename The path and name of the file containing the state reward of the model. This file is optional. * @param transitionRewardFilename The path and name of the file containing the transition rewards of the model. This file is optional. + * @param choiceLabelingFilename The path and name of the file containing the choice labeling of the model. This file is optional. + * @return The parsed Ctmc. */ static storm::models::sparse::Ctmc> parseCtmc(std::string const& transitionsFilename, std::string const & labelingFilename, std::string const & stateRewardFilename = "", - std::string const & transitionRewardFilename = ""); + std::string const & transitionRewardFilename = "", + std::string const & choiceLabelingFilename = ""); + private: @@ -109,12 +118,14 @@ namespace storm { * @param labelingFilename The path and name of the file containing the labels for the states of the model. * @param stateRewardFilename The path and name of the file containing the state reward of the model. This file is optional. * @param transitionRewardFilename The path and name of the file containing the transition rewards of the model. This file is optional. + * @param choiceLabelingFilename The path and name of the file containing the choice labeling of the model. This file is optional. * @return The parsed model encapsulated in a Result structure. */ static Result parseDeterministicModel(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename = "", - std::string const& transitionRewardFilename = ""); + std::string const& transitionRewardFilename = "", + std::string const & choiceLabelingFilename = ""); }; } /* namespace parser */ diff --git a/src/storm/parser/MarkovAutomatonParser.cpp b/src/storm/parser/MarkovAutomatonParser.cpp index d8a709cd9..a42c9c341 100644 --- a/src/storm/parser/MarkovAutomatonParser.cpp +++ b/src/storm/parser/MarkovAutomatonParser.cpp @@ -1,6 +1,7 @@ #include "MarkovAutomatonParser.h" -#include "AtomicPropositionLabelingParser.h" +#include "SparseItemLabelingParser.h" #include "SparseStateRewardParser.h" +#include "NondeterministicSparseTransitionParser.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -12,7 +13,7 @@ namespace storm { namespace parser { template - storm::models::sparse::MarkovAutomaton> MarkovAutomatonParser::parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename) { + storm::models::sparse::MarkovAutomaton> MarkovAutomatonParser::parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename, std::string const& choiceLabelingFilename) { // Parse the transitions of the Markov Automaton. typename storm::parser::MarkovAutomatonSparseTransitionParser::Result transitionResult(storm::parser::MarkovAutomatonSparseTransitionParser::parseMarkovAutomatonTransitions(transitionsFilename)); @@ -21,24 +22,31 @@ namespace storm { storm::storage::SparseMatrix transitionMatrix(transitionResult.transitionMatrixBuilder.build()); // Parse the state labeling. - storm::models::sparse::StateLabeling resultLabeling(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(transitionMatrix.getColumnCount(), labelingFilename)); + storm::models::sparse::StateLabeling resultLabeling(storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(transitionMatrix.getColumnCount(), labelingFilename)); // If given, parse the state rewards file. boost::optional> stateRewards; - if (stateRewardFilename != "") { + if (!stateRewardFilename.empty()) { stateRewards.reset(storm::parser::SparseStateRewardParser::parseSparseStateReward(transitionMatrix.getColumnCount(), stateRewardFilename)); } + + // Only parse transition rewards if a file is given. + boost::optional> transitionRewards; + if (!transitionRewardFilename.empty()) { + transitionRewards = std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFilename, transitionMatrix)); + } + std::unordered_map> rewardModels; - rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(stateRewards, boost::optional>(), boost::optional>()))); + rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(std::move(stateRewards), boost::none, std::move(transitionRewards)))); - // Since Markov Automata do not support transition rewards no path should be given here. - if (transitionRewardFilename != "") { - STORM_LOG_ERROR("Transition rewards are unsupported for Markov automata."); - throw storm::exceptions::WrongFormatException() << "Transition rewards are unsupported for Markov automata."; + // Only parse choice labeling if a file is given. + boost::optional choiceLabeling; + if (!choiceLabelingFilename.empty()) { + choiceLabeling = storm::parser::SparseItemLabelingParser::parseChoiceLabeling(transitionMatrix.getRowCount(), choiceLabelingFilename, transitionMatrix.getRowGroupIndices()); } // Put the pieces together to generate the Markov Automaton. - storm::models::sparse::MarkovAutomaton> resultingAutomaton(std::move(transitionMatrix), std::move(resultLabeling), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), rewardModels); + storm::models::sparse::MarkovAutomaton> resultingAutomaton(std::move(transitionMatrix), std::move(resultLabeling), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(rewardModels), std::move(choiceLabeling)); return resultingAutomaton; } diff --git a/src/storm/parser/MarkovAutomatonParser.h b/src/storm/parser/MarkovAutomatonParser.h index 9508c8302..763ece141 100644 --- a/src/storm/parser/MarkovAutomatonParser.h +++ b/src/storm/parser/MarkovAutomatonParser.h @@ -27,9 +27,10 @@ namespace storm { * @param labelingFilename The name of the file containing the labels for the states of the Markov automaton. * @param stateRewardFilename The name of the file that contains the state reward of the Markov automaton. * @param transitionRewardFilename The name of the file that contains the transition rewards of the Markov automaton. This should be empty as transition rewards are not supported by Markov Automata. + * @param choiceLabelingFilename The name of the file that contains the choice labels. * @return The parsed MarkovAutomaton. */ - static storm::models::sparse::MarkovAutomaton> parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename = "", std::string const& transitionRewardFilename = ""); + static storm::models::sparse::MarkovAutomaton> parseMarkovAutomaton(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename = "", std::string const& transitionRewardFilename = "", std::string const& choiceLabelingFilename = ""); }; } // namespace parser diff --git a/src/storm/parser/NondeterministicModelParser.cpp b/src/storm/parser/NondeterministicModelParser.cpp index e93ca6a23..152fa8943 100644 --- a/src/storm/parser/NondeterministicModelParser.cpp +++ b/src/storm/parser/NondeterministicModelParser.cpp @@ -6,9 +6,8 @@ #include "storm/models/sparse/StandardRewardModel.h" #include "storm/parser/NondeterministicSparseTransitionParser.h" -#include "storm/parser/AtomicPropositionLabelingParser.h" +#include "storm/parser/SparseItemLabelingParser.h" #include "storm/parser/SparseStateRewardParser.h" -#include "storm/parser/SparseChoiceLabelingParser.h" #include "storm/adapters/CarlAdapter.h" #include "storm/utility/macros.h" @@ -25,7 +24,7 @@ namespace storm { uint_fast64_t stateCount = transitions.getColumnCount(); // Parse the state labeling. - storm::models::sparse::StateLabeling labeling(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename)); + storm::models::sparse::StateLabeling labeling(storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename)); // Only parse state rewards if a file is given. boost::optional> stateRewards; @@ -42,8 +41,7 @@ namespace storm { // Only parse choice labeling if a file is given. boost::optional choiceLabeling; if (!choiceLabelingFilename.empty()) { - STORM_LOG_ERROR("Parsing choice labels is currently not implemented"); // TODO - //choiceLabeling = std::move(storm::parser::SparseChoiceLabelingParser::parseChoiceLabeling(transitions.getRowGroupIndices(), choiceLabelingFilename)); + choiceLabeling = storm::parser::SparseItemLabelingParser::parseChoiceLabeling(transitions.getRowCount(), choiceLabelingFilename, transitions.getRowGroupIndices()); } // Construct the result. diff --git a/src/storm/parser/SparseItemLabelingParser.cpp b/src/storm/parser/SparseItemLabelingParser.cpp new file mode 100644 index 000000000..2e98e4673 --- /dev/null +++ b/src/storm/parser/SparseItemLabelingParser.cpp @@ -0,0 +1,254 @@ +#include "storm/parser/SparseItemLabelingParser.h" + +#include +#include +#include + +#include "storm/utility/cstring.h" +#include "storm/parser/MappedFile.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/WrongFormatException.h" +#include "storm/exceptions/FileIoException.h" + +namespace storm { + namespace parser { + + using namespace storm::utility::cstring; + + storm::models::sparse::StateLabeling SparseItemLabelingParser::parseAtomicPropositionLabeling(uint_fast64_t stateCount, std::string const & filename) { + MappedFile file(filename.c_str()); + checkSyntax(filename, file); + + // Create labeling object with given node and label count. + storm::models::sparse::StateLabeling labeling(stateCount); + + // initialize the buffer + char const* buf = file.getData(); + + // add the labels to the labeling + parseLabelNames(filename, labeling, buf); + + // Now parse the assignments of labels to states. + parseDeterministicLabelAssignments(filename, labeling, buf); + + return labeling; + } + + storm::models::sparse::ChoiceLabeling SparseItemLabelingParser::parseChoiceLabeling(uint_fast64_t choiceCount, std::string const& filename, boost::optional> const& nondeterministicChoiceIndices) { + MappedFile file(filename.c_str()); + checkSyntax(filename, file); + + // Create labeling object with given node and label count. + storm::models::sparse::ChoiceLabeling labeling(choiceCount); + + // initialize the buffer + char const* buf = file.getData(); + + // add the labels to the labeling + parseLabelNames(filename, labeling, buf); + + // Now parse the assignments of labels to states. + if (nondeterministicChoiceIndices) { + parseNonDeterministicLabelAssignments(filename, labeling, nondeterministicChoiceIndices.get(), buf); + } else { + parseDeterministicLabelAssignments(filename, labeling, buf); + } + + return labeling; + } + + + void SparseItemLabelingParser::checkSyntax(std::string const & filename, storm::parser::MappedFile const& file) { + char const* buf = file.getData(); + + // First pass: Count the number of propositions. + bool foundDecl = false, foundEnd = false; + size_t cnt = 0; + + // Iterate over tokens until we hit #END or the end of the file. + while(buf[0] != '\0') { + + //Move the buffer to the beginning of the next word. + buf += cnt; + buf = trimWhitespaces(buf); + + // Get the number of characters until the next separator. + cnt = skipWord(buf) - buf; + if (cnt > 0) { + + // If the next token is #DECLARATION: Just skip it. + // If the next token is #END: Stop the search. + // Otherwise increase proposition_count. + if (strncmp(buf, "#DECLARATION", cnt) == 0) { + foundDecl = true; + continue; + } else if (strncmp(buf, "#END", cnt) == 0) { + foundEnd = true; + break; + } + } + } + + // If #DECLARATION or #END have not been found, the file format is wrong. + STORM_LOG_THROW(foundDecl, storm::exceptions::WrongFormatException, "Error while parsing " << filename << ": File header is corrupted (Token #DECLARATION missing - case sensitive)."); + STORM_LOG_THROW(foundEnd, storm::exceptions::WrongFormatException, "Error while parsing " << filename << ": File header is corrupted (Token #END missing - case sensitive)."); + } + + + void SparseItemLabelingParser::parseLabelNames(std::string const & filename, storm::models::sparse::ItemLabeling& labeling, char const*& buf) { + // Prepare a buffer for proposition names. + char proposition[128]; + size_t cnt = 0; + + // Parse proposition names. + // As we already checked the file header, we know that #DECLARATION and #END are tokens in the character stream. + while(buf[0] != '\0') { + + //Move the buffer to the beginning of the next word. + buf += cnt; + buf = trimWhitespaces(buf); + + // Get the number of characters until the next separator. + cnt = skipWord(buf) - buf; + + if (cnt >= sizeof(proposition)) { + + // if token is longer than our buffer, the following strncpy code might get risky... + STORM_LOG_ERROR("Error while parsing " << filename << ": Atomic proposition with length > " << (sizeof(proposition) - 1) << " was found."); + throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": Atomic proposition with length > " << (sizeof(proposition) - 1) << " was found."; + + } else if (cnt > 0) { + + // If the next token is #DECLARATION: Just skip it. + if (strncmp(buf, "#DECLARATION", cnt) == 0) continue; + + // If the next token is #END: Stop the search. + if (strncmp(buf, "#END", cnt) == 0) break; + + // Otherwise copy the token to the buffer, append a trailing null byte and hand it to labeling. + strncpy(proposition, buf, cnt); + proposition[cnt] = '\0'; + labeling.addLabel(proposition); + } + } + + // At this point, the pointer buf is still pointing to our last token, i.e. to #END. + // We want to skip it. + buf += 4; + + // Now eliminate remaining whitespaces such as empty lines and start parsing. + buf = trimWhitespaces(buf); + } + + void SparseItemLabelingParser::parseDeterministicLabelAssignments(std::string const & filename, storm::models::sparse::ItemLabeling& labeling, char const*& buf) { + uint_fast64_t state = 0; + uint_fast64_t lastState = (uint_fast64_t)-1; + uint_fast64_t const startIndexComparison = lastState; + size_t cnt = 0; + char proposition[128]; + + while (buf[0] != '\0') { + + // Parse the state number and iterate over its labels (atomic propositions). + // Stop at the end of the line. + state = checked_strtol(buf, &buf); + + // If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks). + if (state <= lastState && lastState != startIndexComparison) { + STORM_LOG_ERROR("Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously."); + throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously."; + } + + while ((buf[0] != '\r') && (buf[0] != '\n') && (buf[0] != '\0')) { + cnt = skipWord(buf) - buf; + if (cnt == 0) { + + // The next character is a separator. + // If it is a line separator, we continue with next node. + // Otherwise, we skip it and try again. + if (buf[0] == '\n' || buf[0] == '\r') break; + buf++; + } else { + + // Copy the label to the buffer, null terminate it and add it to labeling. + strncpy(proposition, buf, cnt); + proposition[cnt] = '\0'; + + // Has the label been declared in the header? + if(!labeling.containsLabel(proposition)) { + STORM_LOG_ERROR("Error while parsing " << filename << ": Atomic proposition" << proposition << " was found but not declared."); + throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": Atomic proposition" << proposition << " was found but not declared."; + } + if (labeling.isStateLabeling()) { + labeling.asStateLabeling().addLabelToState(proposition, state); + } else { + STORM_LOG_ASSERT(labeling.isChoiceLabeling(), "Unexpected labeling type"); + labeling.asChoiceLabeling().addLabelToChoice(proposition, state); + } + buf += cnt; + } + } + buf = trimWhitespaces(buf); + lastState = state; + } + } + + void SparseItemLabelingParser::parseNonDeterministicLabelAssignments(std::string const & filename, storm::models::sparse::ChoiceLabeling& labeling, std::vector const& nondeterministicChoiceIndices, char const*& buf) { + uint_fast64_t const startIndexComparison = (uint_fast64_t)-1; + uint_fast64_t state = 0; + uint_fast64_t lastState = startIndexComparison; + uint_fast64_t localChoice = 0; + uint_fast64_t lastLocalChoice = startIndexComparison; + size_t cnt = 0; + char proposition[128]; + + while (buf[0] != '\0') { + + // Parse the state and choice number and iterate over its labels (atomic propositions). + // Stop at the end of the line. + state = checked_strtol(buf, &buf); + localChoice = checked_strtol(buf, &buf); + + // If we see this state for the first time, reset the last choice + if (state != lastState) { + lastLocalChoice = startIndexComparison; + } + + // If the state-choice pair has already been read or skipped once there might be a problem with the file (doubled lines, or blocks). + STORM_LOG_THROW(state >= lastState || lastState == startIndexComparison, storm::exceptions::WrongFormatException, "Error while parsing " << filename << ": State " << state << " and Choice " << localChoice << " were found but the state has already been read or skipped previously."); + STORM_LOG_THROW(state != lastState || localChoice > lastLocalChoice || lastLocalChoice == startIndexComparison, storm::exceptions::WrongFormatException, "Error while parsing " << filename << ": State " << state << " and Choice " << localChoice << " were found but the choice has already been read or skipped previously."); + + uint_fast64_t const globalChoice = nondeterministicChoiceIndices[state] + localChoice; + STORM_LOG_THROW(globalChoice < nondeterministicChoiceIndices[state + 1], storm::exceptions::WrongFormatException, "Error while parsing " << filename << ": Invalid choice index " << localChoice << " at state " << state << "."); + + while ((buf[0] != '\r') && (buf[0] != '\n') && (buf[0] != '\0')) { + cnt = skipWord(buf) - buf; + if (cnt == 0) { + + // The next character is a separator. + // If it is a line separator, we continue with next node. + // Otherwise, we skip it and try again. + if (buf[0] == '\n' || buf[0] == '\r') break; + buf++; + } else { + + // Copy the label to the buffer, null terminate it and add it to labeling. + strncpy(proposition, buf, cnt); + proposition[cnt] = '\0'; + + // Has the label been declared in the header? + STORM_LOG_THROW(labeling.containsLabel(proposition), storm::exceptions::WrongFormatException, "Error while parsing " << filename << ": Atomic proposition" << proposition << " was found but not declared."); + + labeling.addLabelToChoice(proposition, globalChoice); + buf += cnt; + } + } + buf = trimWhitespaces(buf); + lastState = state; + lastLocalChoice = localChoice; + } + } + + } // namespace parser +} // namespace storm diff --git a/src/storm/parser/SparseItemLabelingParser.h b/src/storm/parser/SparseItemLabelingParser.h new file mode 100644 index 000000000..4b901ab82 --- /dev/null +++ b/src/storm/parser/SparseItemLabelingParser.h @@ -0,0 +1,82 @@ +#pragma once + +#include +#include +#include + +#include "storm/parser/MappedFile.h" +#include "storm/models/sparse/StateLabeling.h" +#include "storm/models/sparse/ChoiceLabeling.h" + + +namespace storm { + namespace parser { + + /*! + * This class can be used to parse a labeling file. + */ + class SparseItemLabelingParser { + + public: + + /*! + * Parses the given file and returns the resulting state labeling. + * + * @param stateCount The number of states of the model to be labeled. + * @param filename The path and name of the labeling (.lab) file. + * @return The parsed labeling as a StateLabeling object. + */ + static storm::models::sparse::StateLabeling parseAtomicPropositionLabeling(uint_fast64_t stateCount, std::string const &filename); + + /*! + * Parses the given file and returns the resulting choice labeling. + * + * @param choiceCount the number of choices of the model. + * @param filename The name of the file to parse. + * @param nondeterministicChoiceIndices if given, the choices are assumed to be nondeterministic, i.e., + * a choice is specified by a tuple of state index and (local) choice index. + * @return The resulting choice labeling. + */ + static storm::models::sparse::ChoiceLabeling parseChoiceLabeling(uint_fast64_t choiceCount, std::string const& filename, boost::optional> const& nondeterministicChoiceIndices = boost::none); + + private: + + /*! + * Perform syntax checks of the file + * @param file The mapped file + */ + static void checkSyntax(std::string const & filename, storm::parser::MappedFile const& file); + + /*! + * Parses the file header (i.e. the #DECLARATION ... #END construct) and adds the label names to the given labeling + * + * @param labeling the labeling to which label names are added + * @param buf the reference to the file contents + */ + static void parseLabelNames(std::string const & filename, storm::models::sparse::ItemLabeling& labeling, char const*& buf); + + + /*! + * Parses the label assignments assuming that each item is uniquely specified by a single index, e.g., + * * 42 label1 label2 label3 + * + * @param labeling the labeling to which file assignments are added + * @param buf the reference to the file contents + */ + static void parseDeterministicLabelAssignments(std::string const & filename, storm::models::sparse::ItemLabeling& labeling, char const*& buf); + + /*! + * Parses the label assignments assuming that each item is specified by a tuple of indices, e.g., + * * 42 0 label1 label2 + * * 42 1 label2 label3 + * + * @param labeling the labeling to which file assignments are added + * @param nondeterministicChoiceIndices The indices at which the choices of the states begin. + * @param buf the reference to the file contents + */ + static void parseNonDeterministicLabelAssignments(std::string const & filename, storm::models::sparse::ChoiceLabeling& labeling, std::vector const& nondeterministicChoiceIndices, char const*& buf); + + }; + + } // namespace parser +} // namespace storm diff --git a/src/test/parser/AtomicPropositionLabelingParserTest.cpp b/src/test/parser/AtomicPropositionLabelingParserTest.cpp deleted file mode 100644 index 15b51d489..000000000 --- a/src/test/parser/AtomicPropositionLabelingParserTest.cpp +++ /dev/null @@ -1,145 +0,0 @@ -/* - * AtomicPropositionLabelingParserTest.cpp - * - * Created on: 03.03.2014 - * Author: Manuel Sascha Weiand - */ - -#include "gtest/gtest.h" -#include "storm-config.h" -#include "storm/models/sparse/StateLabeling.h" -#include "storm/parser/AtomicPropositionLabelingParser.h" -#include "storm/exceptions/FileIoException.h" -#include "storm/exceptions/WrongFormatException.h" -#include "storm/exceptions/OutOfRangeException.h" - -#include - -TEST(AtomicPropositionLabelingParserTest, NonExistingFile) { - // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"! - ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(0,STORM_TEST_RESOURCES_DIR "/nonExistingFile.not"), storm::exceptions::FileIoException); -} - -TEST(AtomicPropositionLabelingParserTest, BasicParsing) { - // This test is based on a test case from the original MRMC. - - // Parsing the file - storm::models::sparse::StateLabeling labeling = storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(12, STORM_TEST_RESOURCES_DIR "/lab/pctl_general.lab"); - - // Checking whether all propositions are in the labelling - - char phi[] = "phi", psi[] = "psi", smth[] = "smth"; - - ASSERT_TRUE(labeling.containsLabel(phi)); - ASSERT_TRUE(labeling.containsLabel(psi)); - ASSERT_TRUE(labeling.containsLabel(smth)); - - // Testing whether all and only the correct nodes are labeled with "phi" - ASSERT_TRUE(labeling.getStateHasLabel(phi,0)); - ASSERT_TRUE(labeling.getStateHasLabel(phi,1)); - ASSERT_TRUE(labeling.getStateHasLabel(phi,2)); - - ASSERT_FALSE(labeling.getStateHasLabel(phi,3)); - ASSERT_FALSE(labeling.getStateHasLabel(phi,4)); - ASSERT_FALSE(labeling.getStateHasLabel(phi,5)); - ASSERT_FALSE(labeling.getStateHasLabel(phi,6)); - ASSERT_FALSE(labeling.getStateHasLabel(phi,7)); - ASSERT_FALSE(labeling.getStateHasLabel(phi,8)); - ASSERT_FALSE(labeling.getStateHasLabel(phi,9)); - ASSERT_FALSE(labeling.getStateHasLabel(phi,10)); - ASSERT_FALSE(labeling.getStateHasLabel(phi,11)); - - //Testing whether all and only the correct nodes are labeled with "psi" - ASSERT_FALSE(labeling.getStateHasLabel(psi,0)); - ASSERT_FALSE(labeling.getStateHasLabel(psi,1)); - ASSERT_FALSE(labeling.getStateHasLabel(psi,2)); - ASSERT_FALSE(labeling.getStateHasLabel(psi,3)); - ASSERT_FALSE(labeling.getStateHasLabel(psi,4)); - ASSERT_FALSE(labeling.getStateHasLabel(psi,5)); - ASSERT_FALSE(labeling.getStateHasLabel(psi,6)); - ASSERT_FALSE(labeling.getStateHasLabel(psi,7)); - ASSERT_FALSE(labeling.getStateHasLabel(psi,8)); - ASSERT_FALSE(labeling.getStateHasLabel(psi,9)); - ASSERT_FALSE(labeling.getStateHasLabel(psi,10)); - ASSERT_FALSE(labeling.getStateHasLabel(psi,11)); - - //Testing whether all and only the correct nodes are labeled with "smth" - ASSERT_TRUE(labeling.getStateHasLabel(smth,2)); - - ASSERT_FALSE(labeling.getStateHasLabel(smth,0)); - ASSERT_FALSE(labeling.getStateHasLabel(smth,1)); - ASSERT_FALSE(labeling.getStateHasLabel(smth,3)); - ASSERT_FALSE(labeling.getStateHasLabel(smth,4)); - ASSERT_FALSE(labeling.getStateHasLabel(smth,5)); - ASSERT_FALSE(labeling.getStateHasLabel(smth,6)); - ASSERT_FALSE(labeling.getStateHasLabel(smth,7)); - ASSERT_FALSE(labeling.getStateHasLabel(smth,8)); - ASSERT_FALSE(labeling.getStateHasLabel(smth,9)); - ASSERT_FALSE(labeling.getStateHasLabel(smth,10)); - ASSERT_FALSE(labeling.getStateHasLabel(smth,11)); -} - -TEST(AtomicPropositionLabelingParserTest, NoDeclarationTagHeader) { - // No #DECLARATION tag in file - ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_TEST_RESOURCES_DIR "/lab/noDeclarationTag.lab"), storm::exceptions::WrongFormatException); -} - -TEST(AtomicPropositionLabelingParserTest, NoEndTagHeader) { - // No #END tag in file. - ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_TEST_RESOURCES_DIR "/lab/noEndTag.lab"), storm::exceptions::WrongFormatException); -} - -TEST(AtomicPropositionLabelingParserTest, MisspelledDeclarationTagHeader) { - // The #DECLARATION tag is misspelled. - ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_TEST_RESOURCES_DIR "/lab/declarationMisspell.lab"), storm::exceptions::WrongFormatException); -} - -TEST(AtomicPropositionLabelingParserTest, MisspelledEndTagHeader) { - // The #END tag is misspelled. - ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_TEST_RESOURCES_DIR "/lab/endMisspell.lab"), storm::exceptions::WrongFormatException); -} - -TEST(AtomicPropositionLabelingParserTest, NoLabelDeclaredNoneGiven) { - // No label between #DECLARATION and #END and no labels given. - storm::models::sparse::StateLabeling labeling = storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(13, STORM_TEST_RESOURCES_DIR "/lab/noLabelsDecNoneGiven.lab"); - ASSERT_EQ(0ul, labeling.getNumberOfLabels()); - for(uint_fast64_t i = 0; i < 13; i++) { - ASSERT_TRUE(labeling.getLabelsOfState(i).empty()); - } -} - -TEST(AtomicPropositionLabelingParserTest, UndeclaredLabelsGiven) { - // Undeclared labels given. - ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_TEST_RESOURCES_DIR "/lab/undeclaredLabelsGiven.lab"), storm::exceptions::WrongFormatException); -} - -TEST(AtomicPropositionLabelingParserTest, LabelForNonExistentState) { - // The index of one of the state that are to be labeled is higher than the number of states in the model. - ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_TEST_RESOURCES_DIR "/lab/labelForNonexistentState.lab"), storm::exceptions::OutOfRangeException); -} - -// Note: As implemented at the moment, each label given for a state in any line is set to true for that state (logical or over all lines for that state). -// This behavior might not be ideal as multiple lines for one state are not necessary and might indicate a corrupt or wrong file. -TEST(AtomicPropositionLabelingParserTest, DoubledLines) { - // There are multiple lines attributing labels to the same state. - ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(6, STORM_TEST_RESOURCES_DIR "/lab/doubledLines.lab"), storm::exceptions::WrongFormatException); - - // There is a line for a state that has been skipped. - ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(6, STORM_TEST_RESOURCES_DIR "/lab/doubledLinesSkipped.lab"), storm::exceptions::WrongFormatException); -} - -TEST(AtomicPropositionLabelingParserTest, WrongProposition) { - // Swapped the state index and the label at one entry. - ASSERT_THROW(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(3, STORM_TEST_RESOURCES_DIR "/lab/swappedStateAndProposition.lab"), storm::exceptions::WrongFormatException); -} - -TEST(AtomicPropositionLabelingParserTest, Whitespaces) { - // Different configurations of allowed whitespaces are tested. - - // First parse the labeling file without added whitespaces and obtain the hash of its parsed representation. - storm::models::sparse::StateLabeling labeling = storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(13, STORM_TEST_RESOURCES_DIR "/lab/withoutWhitespaces.lab"); - - // Now parse the labeling file with the added whitespaces and compare the hashes. - storm::models::sparse::StateLabeling labeling2 = storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(13, STORM_TEST_RESOURCES_DIR "/lab/withWhitespaces.lab"); - ASSERT_TRUE(labeling == labeling2); -} diff --git a/src/test/parser/SparseItemLabelingParserTest.cpp b/src/test/parser/SparseItemLabelingParserTest.cpp new file mode 100644 index 000000000..bca1c2201 --- /dev/null +++ b/src/test/parser/SparseItemLabelingParserTest.cpp @@ -0,0 +1,165 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "storm/models/sparse/StateLabeling.h" +#include "storm/parser/SparseItemLabelingParser.h" +#include "storm/exceptions/FileIoException.h" +#include "storm/exceptions/WrongFormatException.h" +#include "storm/exceptions/OutOfRangeException.h" + +#include + +TEST(SparseItemLabelingParserTest, NonExistingFile) { + // No matter what happens, please do NOT create a file with the name "nonExistingFile.not"! + ASSERT_THROW(storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(0,STORM_TEST_RESOURCES_DIR "/nonExistingFile.not"), storm::exceptions::FileIoException); +} + +TEST(SparseItemLabelingParserTest, BasicDeterministicParsing) { + // This test is based on a test case from the original MRMC. + + // Parsing the file + storm::models::sparse::StateLabeling labeling = storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(12, STORM_TEST_RESOURCES_DIR "/lab/pctl_general.lab"); + + // Checking whether all propositions are in the labelling + + char phi[] = "phi", psi[] = "psi", smth[] = "smth"; + + ASSERT_TRUE(labeling.containsLabel(phi)); + ASSERT_TRUE(labeling.containsLabel(psi)); + ASSERT_TRUE(labeling.containsLabel(smth)); + + // Testing whether all and only the correct nodes are labeled with "phi" + ASSERT_TRUE(labeling.getStateHasLabel(phi,0)); + ASSERT_TRUE(labeling.getStateHasLabel(phi,1)); + ASSERT_TRUE(labeling.getStateHasLabel(phi,2)); + + ASSERT_FALSE(labeling.getStateHasLabel(phi,3)); + ASSERT_FALSE(labeling.getStateHasLabel(phi,4)); + ASSERT_FALSE(labeling.getStateHasLabel(phi,5)); + ASSERT_FALSE(labeling.getStateHasLabel(phi,6)); + ASSERT_FALSE(labeling.getStateHasLabel(phi,7)); + ASSERT_FALSE(labeling.getStateHasLabel(phi,8)); + ASSERT_FALSE(labeling.getStateHasLabel(phi,9)); + ASSERT_FALSE(labeling.getStateHasLabel(phi,10)); + ASSERT_FALSE(labeling.getStateHasLabel(phi,11)); + + //Testing whether all and only the correct nodes are labeled with "psi" + ASSERT_FALSE(labeling.getStateHasLabel(psi,0)); + ASSERT_FALSE(labeling.getStateHasLabel(psi,1)); + ASSERT_FALSE(labeling.getStateHasLabel(psi,2)); + ASSERT_FALSE(labeling.getStateHasLabel(psi,3)); + ASSERT_FALSE(labeling.getStateHasLabel(psi,4)); + ASSERT_FALSE(labeling.getStateHasLabel(psi,5)); + ASSERT_FALSE(labeling.getStateHasLabel(psi,6)); + ASSERT_FALSE(labeling.getStateHasLabel(psi,7)); + ASSERT_FALSE(labeling.getStateHasLabel(psi,8)); + ASSERT_FALSE(labeling.getStateHasLabel(psi,9)); + ASSERT_FALSE(labeling.getStateHasLabel(psi,10)); + ASSERT_FALSE(labeling.getStateHasLabel(psi,11)); + + //Testing whether all and only the correct nodes are labeled with "smth" + ASSERT_TRUE(labeling.getStateHasLabel(smth,2)); + + ASSERT_FALSE(labeling.getStateHasLabel(smth,0)); + ASSERT_FALSE(labeling.getStateHasLabel(smth,1)); + ASSERT_FALSE(labeling.getStateHasLabel(smth,3)); + ASSERT_FALSE(labeling.getStateHasLabel(smth,4)); + ASSERT_FALSE(labeling.getStateHasLabel(smth,5)); + ASSERT_FALSE(labeling.getStateHasLabel(smth,6)); + ASSERT_FALSE(labeling.getStateHasLabel(smth,7)); + ASSERT_FALSE(labeling.getStateHasLabel(smth,8)); + ASSERT_FALSE(labeling.getStateHasLabel(smth,9)); + ASSERT_FALSE(labeling.getStateHasLabel(smth,10)); + ASSERT_FALSE(labeling.getStateHasLabel(smth,11)); +} + +TEST(SparseItemLabelingParserTest, BasicNondeterministicParsing) { + + std::vector choiceIndices {0, 3, 5, 6, 9, 11}; + + // Parsing the file + storm::models::sparse::ChoiceLabeling labeling = storm::parser::SparseItemLabelingParser::parseChoiceLabeling(11, STORM_TEST_RESOURCES_DIR "/lab/nondet.choicelab", choiceIndices); + + // Checking whether the parsed labeling is correct + ASSERT_TRUE(labeling.containsLabel("alpha")); + EXPECT_EQ(2, labeling.getChoices("alpha").getNumberOfSetBits()); + EXPECT_TRUE(labeling.getChoiceHasLabel("alpha", 0)); + EXPECT_TRUE(labeling.getChoiceHasLabel("alpha", 1)); + + ASSERT_TRUE(labeling.containsLabel("beta")); + EXPECT_EQ(3, labeling.getChoices("beta").getNumberOfSetBits()); + EXPECT_TRUE(labeling.getChoiceHasLabel("beta", 1)); + EXPECT_TRUE(labeling.getChoiceHasLabel("beta", 3)); + EXPECT_TRUE(labeling.getChoiceHasLabel("beta", 8)); + + ASSERT_TRUE(labeling.containsLabel("gamma")); + EXPECT_EQ(1, labeling.getChoices("gamma").getNumberOfSetBits()); + EXPECT_TRUE(labeling.getChoiceHasLabel("gamma", 2)); + + ASSERT_TRUE(labeling.containsLabel("delta")); + EXPECT_TRUE(labeling.getChoices("delta").empty()); +} + +TEST(SparseItemLabelingParserTest, NoDeclarationTagHeader) { + // No #DECLARATION tag in file + ASSERT_THROW(storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(3, STORM_TEST_RESOURCES_DIR "/lab/noDeclarationTag.lab"), storm::exceptions::WrongFormatException); +} + +TEST(SparseItemLabelingParserTest, NoEndTagHeader) { + // No #END tag in file. + ASSERT_THROW(storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(3, STORM_TEST_RESOURCES_DIR "/lab/noEndTag.lab"), storm::exceptions::WrongFormatException); +} + +TEST(SparseItemLabelingParserTest, MisspelledDeclarationTagHeader) { + // The #DECLARATION tag is misspelled. + ASSERT_THROW(storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(3, STORM_TEST_RESOURCES_DIR "/lab/declarationMisspell.lab"), storm::exceptions::WrongFormatException); +} + +TEST(SparseItemLabelingParserTest, MisspelledEndTagHeader) { + // The #END tag is misspelled. + ASSERT_THROW(storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(3, STORM_TEST_RESOURCES_DIR "/lab/endMisspell.lab"), storm::exceptions::WrongFormatException); +} + +TEST(SparseItemLabelingParserTest, NoLabelDeclaredNoneGiven) { + // No label between #DECLARATION and #END and no labels given. + storm::models::sparse::StateLabeling labeling = storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(13, STORM_TEST_RESOURCES_DIR "/lab/noLabelsDecNoneGiven.lab"); + ASSERT_EQ(0ul, labeling.getNumberOfLabels()); + for(uint_fast64_t i = 0; i < 13; i++) { + ASSERT_TRUE(labeling.getLabelsOfState(i).empty()); + } +} + +TEST(SparseItemLabelingParserTest, UndeclaredLabelsGiven) { + // Undeclared labels given. + ASSERT_THROW(storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(3, STORM_TEST_RESOURCES_DIR "/lab/undeclaredLabelsGiven.lab"), storm::exceptions::WrongFormatException); +} + +TEST(SparseItemLabelingParserTest, LabelForNonExistentState) { + // The index of one of the state that are to be labeled is higher than the number of states in the model. + ASSERT_THROW(storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(3, STORM_TEST_RESOURCES_DIR "/lab/labelForNonexistentState.lab"), storm::exceptions::OutOfRangeException); +} + +// Note: As implemented at the moment, each label given for a state in any line is set to true for that state (logical or over all lines for that state). +// This behavior might not be ideal as multiple lines for one state are not necessary and might indicate a corrupt or wrong file. +TEST(SparseItemLabelingParserTest, DoubledLines) { + // There are multiple lines attributing labels to the same state. + ASSERT_THROW(storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(6, STORM_TEST_RESOURCES_DIR "/lab/doubledLines.lab"), storm::exceptions::WrongFormatException); + + // There is a line for a state that has been skipped. + ASSERT_THROW(storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(6, STORM_TEST_RESOURCES_DIR "/lab/doubledLinesSkipped.lab"), storm::exceptions::WrongFormatException); +} + +TEST(SparseItemLabelingParserTest, WrongProposition) { + // Swapped the state index and the label at one entry. + ASSERT_THROW(storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(3, STORM_TEST_RESOURCES_DIR "/lab/swappedStateAndProposition.lab"), storm::exceptions::WrongFormatException); +} + +TEST(SparseItemLabelingParserTest, Whitespaces) { + // Different configurations of allowed whitespaces are tested. + + // First parse the labeling file without added whitespaces and obtain the hash of its parsed representation. + storm::models::sparse::StateLabeling labeling = storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(13, STORM_TEST_RESOURCES_DIR "/lab/withoutWhitespaces.lab"); + + // Now parse the labeling file with the added whitespaces and compare the hashes. + storm::models::sparse::StateLabeling labeling2 = storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(13, STORM_TEST_RESOURCES_DIR "/lab/withWhitespaces.lab"); + ASSERT_TRUE(labeling == labeling2); +}