Skip to content

Commit

Permalink
Introduce StateDescription class and add template arguments for runni…
Browse files Browse the repository at this point in the history
…ng SMC with and without the ExplorationInformation data (#20)

Signed-off-by: Marco Lampacrescia <[email protected]>
  • Loading branch information
MarcoLm993 authored Oct 22, 2024
1 parent a889d0a commit 02fadd6
Show file tree
Hide file tree
Showing 17 changed files with 572 additions and 640 deletions.
130 changes: 130 additions & 0 deletions include/model_checker/state_expansion_handler.hpp
Original file line number Diff line number Diff line change
@@ -0,0 +1,130 @@
/*
* Copyright (c) 2024 Robert Bosch GmbH and its subsidiaries
*
* This file is part of smc_storm.
*
* smc_storm is free software: you can redistribute it and/or modify it under the terms of
* the GNU General Public License as published by the Free Software Foundation, either
* version 3 of the License, or (at your option) any later version.
*
* smc_storm is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY;
* without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
* See the GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License along with smc_storm.
* If not, see <https://www.gnu.org/licenses/>.
*/

#pragma once

#include <memory>

#include <storm/generator/CompressedState.h>
#include <storm/storage/sparse/StateStorage.h>

#include "samples/exploration_information.hpp"

namespace smc_storm {
namespace model_checker {

/*!
* @brief Class that loads an input model and property to generate states and verify if the input property holds.
* @tparam StateType Variable type to identify states and actions
* @tparam ValueType Variable type of computed results (e.g. rewards)
*/
template <typename StateType, typename ValueType>
class StateExpansionHandler {
public:
StateExpansionHandler();

/*!
* @brief Init the state storage structures, if required
* @param state_size the dimension of the model's state
*/
void init(const uint64_t state_size);

/*!
* @brief Callback to process the next states from the one under expansion. It must assign a numeric ID to them
* @param state The state ID to process
* @return The int ID associated to the processed next state
*/
uint32_t stateExpansionCallback(const storm::generator::CompressedState& state);
};

template <typename ValueType>
class StateExpansionHandler<storm::generator::CompressedState, ValueType> {
private:
std::vector<storm::generator::CompressedState> _next_states;
const storm::storage::Murmur3BitVectorHash<uint32_t> _hash_f;

public:
StateExpansionHandler() : _hash_f(storm::storage::Murmur3BitVectorHash<uint32_t>{}) {}

void init([[maybe_unused]] const uint64_t state_size) {}

uint32_t stateExpansionCallback(const storm::generator::CompressedState& state) {
const uint32_t state_id = _next_states.size();
_next_states.emplace_back(state);
return state_id;
}

/*!
* @brief Get the next states generated by the last state expansion
* @return The next states generated by the last state expansion
*/
inline const std::vector<storm::generator::CompressedState>& getNextStates() const {
return _next_states;
}

/*!
* @brief Clear the next states generated by the last state expansion
*/
inline void clearNextStates() {
_next_states.clear();
}

/*!
* @brief Get the hash value of the compressed state
* @param compressed_state The compressed state to hash
* @return The hash value of the compressed state
*/
inline const uint32_t getHashValue(const storm::generator::CompressedState& compressed_state) const {
return _hash_f(compressed_state);
}
};

template <typename ValueType>
class StateExpansionHandler<uint32_t, ValueType> {
private:
std::unique_ptr<storm::storage::sparse::StateStorage<uint32_t>> _state_storage_ptr;
samples::ExplorationInformation<uint32_t, ValueType> _exploration_information;

public:
StateExpansionHandler() {}

void init(const uint64_t state_size) {
_state_storage_ptr = std::make_unique<storm::storage::sparse::StateStorage<uint32_t>>(state_size);
}

uint32_t stateExpansionCallback(const storm::generator::CompressedState& state) {
uint32_t new_index = _state_storage_ptr->getNumberOfStates();
// Check, if the state was already registered.
std::pair<uint32_t, std::size_t> actual_index_bucket_pair = (_state_storage_ptr->stateToId).findOrAddAndGetBucket(state, new_index);

if (actual_index_bucket_pair.first == new_index) {
_exploration_information.addUnexploredState(new_index, state);
}
return actual_index_bucket_pair.first;
}

/*!
* @brief Get the reference to the previous explored states container
* @return ExplorationInformation instance
*/
samples::ExplorationInformation<uint32_t, ValueType>& getExplorationInformation() {
return _exploration_information;
}
};

} // namespace model_checker
} // namespace smc_storm
109 changes: 40 additions & 69 deletions include/model_checker/state_generation.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -22,36 +22,37 @@

#include <storm/generator/CompressedState.h>
#include <storm/generator/NextStateGenerator.h>
#include <storm/storage/sparse/StateStorage.h>
#include <storm/storage/SymbolicModelDescription.h>

#include "model_checker/state_expansion_handler.hpp"
#include "state_properties/property_description.hpp"
#include "state_properties/state_description.hpp"

namespace smc_storm {
namespace samples {
template <typename StateType, typename ValueType>
class ExplorationInformation;
} // namespace samples

namespace model_checker {
template <typename StateType>
concept StoreExpandedStates = !std::is_same_v<StateType, storm::generator::CompressedState>;

/*!
* @brief Class that loads an input model and property to generate states and verify if the input property holds.
* @tparam StateType Variab;e type to identify states and actions
* @tparam StateType Variable type to identify states and actions
* @tparam ValueType Variable type of computed results (e.g. rewards)
*/
template <typename StateType, typename ValueType>
class StateGeneration {
using StateIdType = std::conditional_t<StoreExpandedStates<StateType>, StateType, uint32_t>;

public:
/*!
* @brief Extension of the constructor above, in case we evaluate Rewards
* @param model The model to generate the next states from
* @param formula The formula to evaluate on the generated states
* @param reward_model Name of the reward model to use for assigning costs on states and actions. Empty for P properties
* @param exploration_information Structure that keeps track of the already explored states
* @param store_compressed_states Whether to store the explored compressed states (for trace generation)
*/
StateGeneration(
const storm::storage::SymbolicModelDescription& model, const storm::logic::Formula& formula, const std::string& reward_model,
samples::ExplorationInformation<StateType, ValueType>& exploration_information);
const bool store_compressed_states);

/*!
* @brief Get the variable information related to the loaded model
Expand All @@ -62,91 +63,61 @@ class StateGeneration {
}

/*!
* @brief Check if a reward model is loaded and therefore it needs to be evaluated
* @return true if we loaded a reward model, false otherwise
*/
inline bool rewardLoaded() const {
return std::numeric_limits<size_t>::max() != _reward_model_index;
}

/*!
* @brief Get the index of the reward model of our interest
* @return Index matching to the reward model we are evaluating
* @brief Load the initial state in the NextStateGenerator (basically a model reset).
*/
inline size_t getRewardIndex() const {
return _reward_model_index;
}
void loadInitialState();

/*!
* @brief Load a compressed state in the NextStateGenerator
* @param state The compressed state to load
*/
void load(const storm::generator::CompressedState& state);
void load(const StateType& state_id);

/*!
* @brief Get the initial states of the loaded model
* @return A list of state IDs
*/
std::vector<StateType> getInitialStates();
const state_properties::StateDescription<StateType, ValueType>& processLoadedState();

/*!
* @brief Expand the loaded state to get the next states
* @return A generator used to access the generated information
*/
storm::generator::StateBehavior<ValueType, StateType> expand();

void computeInitialStates();

StateType getFirstInitialState() const;
const state_properties::PropertyDescription& getPropertyDescription() const {
return _property_description;
}

std::size_t getNumberOfInitialStates() const;
private:
void initStateToIdCallback();

/*!
* @brief Check whether the loaded state satisfies the condition formula
* @return true if the condition formula is satisfied, false otherwise
*/
bool isConditionState() const;
void initNextStateGenerator(const storm::storage::SymbolicModelDescription& model, const std::string& reward_model);

/*!
* @brief Check whether the loaded state satisfies the target formula
* @return true if the target formula is satisfied, false otherwise
* @brief Expand the loaded state to get the next states
* @return A generator used to access the generated information
*/
bool isTargetState() const;
storm::generator::StateBehavior<ValueType, StateType> expand();

/*!
* @brief Getter for the min amount of steps to compute before checking for target and condition formulae
* @return The lower bound of the property
*/
inline size_t getLowerBound() const {
return _property_description.getLowerBound();
}
void exploreState(const StateIdType state_id, const storm::generator::CompressedState& compressed_state);

/*!
* @brief Getter for the max amount of steps, after which the property is marked as unsatisfied
* @return The upper bound of the property
*/
inline size_t getUpperBound() const {
return _property_description.getUpperBound();
}
void computeInitialStates();

/*!
* @brief Flag indicating that a terminal state should be considered as verified, regardless of the target formula
* @return true if any terminal state that does not break the condition formula is verified, false otherwise
* @brief Check if a reward model is loaded and therefore it needs to be evaluated
* @return true if we loaded a reward model, false otherwise
*/
inline bool getIsTerminalVerified() const {
return _property_description.getIsTerminalVerified();
inline bool rewardLoaded() const {
return std::numeric_limits<size_t>::max() != _reward_model_index;
}

private:
void initStateToIdCallback(samples::ExplorationInformation<StateType, ValueType>& exploration_information);
// Generator extracting the next states from the current one and the input model.
std::unique_ptr<storm::generator::NextStateGenerator<ValueType, StateIdType>> _generator_ptr;
// Current state.
StateType _loaded_state;
std::unique_ptr<state_properties::StateDescription<StateType, ValueType>> _state_description_ptr;
// Vector of initial states (normally only one).
std::vector<StateType> _initial_states;

std::unique_ptr<storm::generator::NextStateGenerator<ValueType, StateType>> _generator_ptr;
std::unique_ptr<storm::storage::sparse::StateStorage<StateType>> _state_storage_ptr;
model_checker::StateExpansionHandler<StateType, ValueType> _state_expansion_handler;

state_properties::PropertyDescription _property_description;
size_t _reward_model_index = std::numeric_limits<size_t>::max();

std::function<StateType(const storm::generator::CompressedState&)> _state_to_id_callback;
const bool _store_compressed_states;

std::function<StateIdType(const storm::generator::CompressedState&)> _state_to_id_callback;
};

} // namespace model_checker
Expand Down
23 changes: 4 additions & 19 deletions include/model_checker/statistical_model_checking_engine.hpp
Original file line number Diff line number Diff line change
Expand Up @@ -58,13 +58,13 @@ class StateGeneration;
/*!
* @brief The implementation of the ModelChecking engine
* @tparam ModelType Definition of the kind of model to evaluate (e.g. DTMC, MDP, ...)
* @tparam StateType Variable type used to identify the states in the model
* @tparam StoreExploredStates Boolean flag to enable the storage of the generated traces
*/
template <typename ModelType, typename StateType = uint32_t>
template <typename ModelType, bool StoreExploredStates>
class StatisticalModelCheckingEngine : public storm::modelchecker::AbstractModelChecker<ModelType> {
public:
typedef typename ModelType::ValueType ValueType;
typedef StateType ActionType;
typedef std::conditional_t<StoreExploredStates, uint32_t, storm::generator::CompressedState> StateType;

/*!
* @brief Constructor for the StatisticalModelCheckingEngine
Expand Down Expand Up @@ -131,26 +131,11 @@ class StatisticalModelCheckingEngine : public storm::modelchecker::AbstractModel
/*!
* @brief Sample a single path until we reach a state it doesn't make sense to expand further
* @param state_generation A representation of the model, to sample the states from
* @param exploration_information Information about the previous explorations (to optimize computation)
* @param model_sampler Object used to randomly sample next action and states
* @return A pair with the Information attached to the reached state and the accumulated reward
*/
samples::TraceInformation samplePathFromInitialState(
StateGeneration<StateType, ValueType>& state_generation,
samples::ExplorationInformation<StateType, ValueType>& exploration_information,
const samples::ModelSampling<StateType, ValueType>& model_sampler) const;

/*!
* @brief Explore a single, unexplored state
* @param state_generation A representation of the model, to sample the states from
* @param current_state_id The ID of the state we are exploring
* @param currentState A compressed representation of the actual state
* @param exploration_information Information about the previous explorations (to optimize computation)
* @return A description of the input state for evaluation
*/
state_properties::StateInfoType exploreState(
StateGeneration<StateType, ValueType>& state_generation, const StateType& current_state_id,
samples::ExplorationInformation<StateType, ValueType>& exploration_information) const;
StateGeneration<StateType, ValueType>& state_generation, const samples::ModelSampling<StateType, ValueType>& model_sampler) const;

// The model to check.
const storm::storage::SymbolicModelDescription _model;
Expand Down
Loading

0 comments on commit 02fadd6

Please sign in to comment.