sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Switched to more elegant solution to query initial states of a model. 

Former-commit-id: 9a5c90c5d5
tempestpy_adaptions
dehnert 11 years ago
parent
84f1b192b4
commit
a99bdf1b17
6 changed files with 22 additions and 43 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 8
      src/counterexamples/MinimalLabelSetGenerator.h
  2. 20
      src/modelchecker/csl/AbstractModelChecker.h
  3. 12
      src/modelchecker/ltl/AbstractModelChecker.h
  4. 13
      src/modelchecker/prctl/AbstractModelChecker.h
  5. 6
      src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
  6. 6
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.h

8
src/counterexamples/MinimalLabelSetGenerator.h
View File

@ -339,7 +339,7 @@ namespace storm {
variableNameBuffer.str("");
variableNameBuffer.clear();
variableNameBuffer << "p" << state;
error = GRBaddvar(model, 0, nullptr, nullptr, maximizeProbability ? (labeledMdp.getLabeledStates("init").get(state) ? -0.5 : 0) : 0, 0.0, 1.0, GRB_CONTINUOUS, variableNameBuffer.str().c_str());
error = GRBaddvar(model, 0, nullptr, nullptr, maximizeProbability ? (labeledMdp.getInitialStates().get(state) ? -0.5 : 0) : 0, 0.0, 1.0, GRB_CONTINUOUS, variableNameBuffer.str().c_str());
if (error) {
LOG4CPLUS_ERROR(logger, "Could not create Gurobi variable (" << GRBgeterrormsg(env) << ").");
throw storm::exceptions::InvalidStateException() << "Could not create Gurobi variable (" << GRBgeterrormsg(env) << ").";
@ -492,7 +492,7 @@ namespace storm {
static uint_fast64_t assertProbabilityGreaterThanThreshold(GRBenv* env, GRBmodel* model, storm::models::Mdp<T> const& labeledMdp, VariableInformation const& variableInformation, T probabilityThreshold) {
uint_fast64_t numberOfConstraintsCreated = 0;
int error = 0;
storm::storage::BitVector const& initialStates = labeledMdp.getLabeledStates("init");
storm::storage::BitVector const& initialStates = labeledMdp.getInitialStates();
if (initialStates.getNumberOfSetBits() != 1) {
LOG4CPLUS_ERROR(logger, "Must have exactly one initial state, but got " << initialStates.getNumberOfSetBits() << "instead.");
throw storm::exceptions::InvalidStateException() << "Must have exactly one initial state, but got " << initialStates.getNumberOfSetBits() << "instead.";
@ -792,7 +792,7 @@ namespace storm {
// For all states except for the initial state, assert that there is a selected incoming transition
// in the subsystem if there is one selected action in the current state.
if (!labeledMdp.getLabeledStates("init").get(state)) {
if (!labeledMdp.getInitialStates().get(state)) {
std::vector<int> variables;
std::vector<double> coefficients;
@ -1035,7 +1035,7 @@ namespace storm {
// Check whether the model was optimized, so we can read off the solution.
if (checkGurobiModelIsOptimized(env, model)) {
double reachabilityProbability = 0;
storm::storage::BitVector const& initialStates = labeledMdp.getLabeledStates("init");
storm::storage::BitVector const& initialStates = labeledMdp.getInitialStates();
for (auto initialState : initialStates) {
error = GRBgetdblattrelement(model, GRB_DBL_ATTR_X, variableInformation.stateToProbabilityVariableIndexMap.at(initialState), &reachabilityProbability);
if (error) {

20
src/modelchecker/csl/AbstractModelChecker.h
View File

@ -130,22 +130,18 @@ public:
std::cout << std::endl;
LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString());
std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl;
storm::storage::BitVector* result = nullptr;
storm::storage::BitVector result;
try {
result = stateFormula.check(*this);
LOG4CPLUS_INFO(logger, "Result for initial states:");
std::cout << "Result for initial states:" << std::endl;
for (auto initialState : model.getLabeledStates("init")) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied"));
std::cout << "\t" << initialState << ": " << result->get(initialState) << std::endl;
for (auto initialState : model.getInitialStates()) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied"));
std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl;
}
delete result;
} catch (std::exception& e) {
std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl;
LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property.");
if (result != nullptr) {
delete result;
}
}
std::cout << std::endl << "-------------------------------------------" << std::endl;
}
@ -160,21 +156,17 @@ public:
std::cout << std::endl;
LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString());
std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl;
std::vector<Type>* result = nullptr;
std::vector<Type> result;
try {
result = this->checkNoBoundOperator(noBoundFormula);
LOG4CPLUS_INFO(logger, "Result for initial states:");
std::cout << "Result for initial states:" << std::endl;
for (auto initialState : model.getLabeledStates("init")) {
for (auto initialState : model.getInitialStates()) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]);
std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
}
delete result;
} catch (std::exception& e) {
std::cout << "Error during computation: " << e.what() << " Skipping property." << std::endl;
if (result != nullptr) {
delete result;
}
}
std::cout << std::endl << "-------------------------------------------" << std::endl;
}

12
src/modelchecker/ltl/AbstractModelChecker.h
View File

@ -114,22 +114,18 @@ public:
std::cout << std::endl;
LOG4CPLUS_INFO(logger, "Model checking formula\t" << ltlFormula.toString());
std::cout << "Model checking formula:\t" << ltlFormula.toString() << std::endl;
storm::storage::BitVector* result = nullptr;
storm::storage::BitVector result;
try {
result = ltlFormula.check(*this);
LOG4CPLUS_INFO(logger, "Result for initial states:");
std::cout << "Result for initial states:" << std::endl;
for (auto initialState : model.getLabeledStates("init")) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied"));
std::cout << "\t" << initialState << ": " << result->get(initialState) << std::endl;
for (auto initialState : model.getInitialStates()) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied"));
std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl;
}
delete result;
} catch (std::exception& e) {
std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl;
LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property.");
if (result != nullptr) {
delete result;
}
}
std::cout << std::endl << "-------------------------------------------" << std::endl;
}

13
src/modelchecker/prctl/AbstractModelChecker.h
View File

@ -120,15 +120,6 @@ public:
}
}
/*!
* Retrieves the initial states of the model.
*
* @return A bit vector that represents the initial states of the model.
*/
storm::storage::BitVector const& getInitialStates() const {
return model.getLabeledStates("init");
}
/*!
* Checks the given abstract prctl formula on the model and prints the result (depending on the actual type of the formula)
* for all initial states, i.e. states that carry the atomic proposition "init".
@ -158,7 +149,7 @@ public:
result = stateFormula.check(*this);
LOG4CPLUS_INFO(logger, "Result for initial states:");
std::cout << "Result for initial states:" << std::endl;
for (auto initialState : this->getInitialStates()) {
for (auto initialState : model.getInitialStates()) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied"));
std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl;
}
@ -184,7 +175,7 @@ public:
result = this->checkNoBoundOperator(noBoundFormula);
LOG4CPLUS_INFO(logger, "Result for initial states:");
std::cout << "Result for initial states:" << std::endl;
for (auto initialState : this->getInitialStates()) {
for (auto initialState : model.getInitialStates()) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result[initialState]);
std::cout << "\t" << initialState << ": " << result[initialState] << std::endl;
}

6
src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
View File

@ -98,7 +98,7 @@ public:
// Check if we already know the result (i.e. probability 0) for all initial states and
// don't compute anything in this case.
if (this->getInitialStates().isDisjointFrom(statesWithProbabilityGreater0)) {
if (this->getModel().getInitialStates().isDisjointFrom(statesWithProbabilityGreater0)) {
LOG4CPLUS_INFO(logger, "The probabilities for the initial states were determined in a preprocessing step."
<< " No exact probabilities were computed.");
// Set the values for all maybe-states to 0.5 to indicate that their probability values are not 0 (and
@ -251,7 +251,7 @@ public:
std::vector<Type> result(this->getModel().getNumberOfStates());
// Check whether we need to compute exact probabilities for some states.
if (this->getInitialStates().isDisjointFrom(maybeStates) || qualitative) {
if (this->getModel().getInitialStates().isDisjointFrom(maybeStates) || qualitative) {
if (qualitative) {
LOG4CPLUS_INFO(logger, "The formula was checked qualitatively. No exact probabilities were computed.");
} else {
@ -409,7 +409,7 @@ public:
std::vector<Type> result(this->getModel().getNumberOfStates());
// Check whether we need to compute exact rewards for some states.
if (this->getInitialStates().isDisjointFrom(maybeStates)) {
if (this->getModel().getInitialStates().isDisjointFrom(maybeStates)) {
LOG4CPLUS_INFO(logger, "The rewards for the initial states were determined in a preprocessing step."
<< " No exact rewards were computed.");
// Set the values for all maybe-states to 1 to indicate that their reward values

6
src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
View File

@ -102,7 +102,7 @@ namespace storm {
// Check if we already know the result (i.e. probability 0) for all initial states and
// don't compute anything in this case.
if (this->getInitialStates().isDisjointFrom(statesWithProbabilityGreater0)) {
if (this->getModel().getInitialStates().isDisjointFrom(statesWithProbabilityGreater0)) {
LOG4CPLUS_INFO(logger, "The probabilities for the initial states were determined in a preprocessing step."
<< " No exact probabilities were computed.");
// Set the values for all maybe-states to 0.5 to indicate that their probability values are not 0 (and
@ -282,7 +282,7 @@ namespace storm {
std::vector<Type> result(this->getModel().getNumberOfStates());
// Check whether we need to compute exact probabilities for some states.
if (this->getInitialStates().isDisjointFrom(maybeStates) || qualitative) {
if (this->getModel().getInitialStates().isDisjointFrom(maybeStates) || qualitative) {
if (qualitative) {
LOG4CPLUS_INFO(logger, "The formula was checked qualitatively. No exact probabilities were computed.");
} else {
@ -466,7 +466,7 @@ namespace storm {
std::vector<Type> result(this->getModel().getNumberOfStates());
// Check whether we need to compute exact rewards for some states.
if (this->getInitialStates().isDisjointFrom(maybeStates)) {
if (this->getModel().getInitialStates().isDisjointFrom(maybeStates)) {
LOG4CPLUS_INFO(logger, "The rewards for the initial states were determined in a preprocessing step."
<< " No exact rewards were computed.");
// Set the values for all maybe-states to 1 to indicate that their reward values

Write Preview
Loading…
Cancel
Save