Skip to content

Add scheduler to ExplicitQualitativeCheckResult #832

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
lukovdm wants to merge 7 commits into
base: master
Choose a base branch
from
Open

Add scheduler to ExplicitQualitativeCheckResult #832

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
83d4b50
Add ValueType to ExplicitQualitativeCheckResult
lukovdm Nov 26, 2025
ee9f051
Remember scheduler from quantitative scheduler when applying bounds
lukovdm Nov 26, 2025
1868e44
Export schedulers for qualitative models in the cli
lukovdm Nov 26, 2025
0da7fd8
Fix test
lukovdm Dec 3, 2025
798d3e4
Format
lukovdm Dec 3, 2025
73e73d8
remove weird git thing
lukovdm Dec 3, 2025
f3f81e1
fix one ValueType
lukovdm Dec 3, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 8 additions & 1 deletion src/storm-cli-utilities/model-handling.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1302,7 +1302,7 @@ void verifyModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const&

std::unique_ptr<storm::modelchecker::CheckResult> filter;
if (filterForInitialStates) {
filter = std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(sparseModel->getInitialStates());
filter = std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult<ValueType>>(sparseModel->getInitialStates());
} else if (!states->isTrueFormula()) { // No need to apply filter if it is the formula 'true'
filter = storm::api::verifyWithSparseEngine<ValueType>(mpi.env, sparseModel, storm::api::createTask<ValueType>(states, false));
}
Expand Down Expand Up @@ -1348,6 +1348,13 @@ void verifyModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const&
auto const& paretoRes = result->template asExplicitParetoCurveCheckResult<ValueType>();
storm::api::exportParetoScheduler(sparseModel, paretoRes.getPoints(), paretoRes.getSchedulers(), schedulerExportPath.string());
}
} else if (result->isExplicitQualitativeCheckResult()) {
if constexpr (storm::IsIntervalType<ValueType>) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export for interval models is not supported.");
} else {
storm::api::exportScheduler(sparseModel, result->template asExplicitQualitativeCheckResult<ValueType>().getScheduler(),
schedulerExportPath.string());
}
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export not supported for this value type.");
}
Expand Down
2 changes: 1 addition & 1 deletion src/storm-counterexamples/api/counterexamples.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ std::shared_ptr<storm::counterexamples::Counterexample> computeKShortestPathCoun

storm::logic::EventuallyFormula const& eventuallyFormula = subformula.asEventuallyFormula();
std::unique_ptr<storm::modelchecker::CheckResult> subResult = modelchecker.check(env, eventuallyFormula.getSubformula());
storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult();
storm::modelchecker::ExplicitQualitativeCheckResult<double> const& subQualitativeResult = subResult->template asExplicitQualitativeCheckResult<double>();

// Check if counterexample is even possible
storm::storage::BitVector phiStates(model->getNumberOfStates(), true);
Expand Down
6 changes: 3 additions & 3 deletions src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1023,8 +1023,8 @@ class MILPMinimalLabelSetGenerator {
std::unique_ptr<storm::modelchecker::CheckResult> leftResult = modelchecker.check(env, untilFormula.getLeftSubformula());
std::unique_ptr<storm::modelchecker::CheckResult> rightResult = modelchecker.check(env, untilFormula.getRightSubformula());

storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult->asExplicitQualitativeCheckResult();
storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult->asExplicitQualitativeCheckResult();
storm::modelchecker::ExplicitQualitativeCheckResult<T> const& leftQualitativeResult = leftResult->template asExplicitQualitativeCheckResult<T>();
storm::modelchecker::ExplicitQualitativeCheckResult<T> const& rightQualitativeResult = rightResult->template asExplicitQualitativeCheckResult<T>();

phiStates = leftQualitativeResult.getTruthValuesVector();
psiStates = rightQualitativeResult.getTruthValuesVector();
Expand All @@ -1033,7 +1033,7 @@ class MILPMinimalLabelSetGenerator {

std::unique_ptr<storm::modelchecker::CheckResult> subResult = modelchecker.check(env, eventuallyFormula.getSubformula());

storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult();
storm::modelchecker::ExplicitQualitativeCheckResult<T> const& subQualitativeResult = subResult->template asExplicitQualitativeCheckResult<T>();

phiStates = storm::storage::BitVector(mdp.getNumberOfStates(), true);
psiStates = subQualitativeResult.getTruthValuesVector();
Expand Down
6 changes: 3 additions & 3 deletions src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2157,8 +2157,8 @@ class SMTMinimalLabelSetGenerator {
std::unique_ptr<storm::modelchecker::CheckResult> leftResult = modelchecker.check(env, untilFormula.getLeftSubformula());
std::unique_ptr<storm::modelchecker::CheckResult> rightResult = modelchecker.check(env, untilFormula.getRightSubformula());

storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult->asExplicitQualitativeCheckResult();
storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult->asExplicitQualitativeCheckResult();
storm::modelchecker::ExplicitQualitativeCheckResult<T> const& leftQualitativeResult = leftResult->template asExplicitQualitativeCheckResult<T>();
storm::modelchecker::ExplicitQualitativeCheckResult<T> const& rightQualitativeResult = rightResult->template asExplicitQualitativeCheckResult<T>();

result.phiStates = leftQualitativeResult.getTruthValuesVector();
result.psiStates = rightQualitativeResult.getTruthValuesVector();
Expand All @@ -2167,7 +2167,7 @@ class SMTMinimalLabelSetGenerator {

std::unique_ptr<storm::modelchecker::CheckResult> subResult = modelchecker.check(env, eventuallyFormula.getSubformula());

storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult();
storm::modelchecker::ExplicitQualitativeCheckResult<T> const& subQualitativeResult = subResult->template asExplicitQualitativeCheckResult<T>();

result.phiStates = storm::storage::BitVector(model.getNumberOfStates(), true);
result.psiStates = subQualitativeResult.getTruthValuesVector();
Expand Down
2 changes: 1 addition & 1 deletion src/storm-dft/modelchecker/DFTModelChecker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -461,7 +461,7 @@ std::vector<ValueType> DFTModelChecker<ValueType>::checkModel(std::shared_ptr<st
storm::api::verifyWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(property, true)));

if (result) {
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult<ValueType>(model->getInitialStates()));
ValueType resultValue = result->asExplicitQuantitativeCheckResult<ValueType>().getValueMap().begin()->second;
results.push_back(resultValue);
} else {
Expand Down
2 changes: 1 addition & 1 deletion src/storm-pars-cli/sampling.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -115,7 +115,7 @@ void verifyPropertiesAtSamplePoints(ModelType const& model, cli::SymbolicInput c
valuationWatch.stop();

if (result) {
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model.getInitialStates()));
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult<SolveValueType>(model.getInitialStates()));
}
printInitialStatesResult<ValueType>(result, &valuationWatch, &valuation);

Expand Down
2 changes: 1 addition & 1 deletion src/storm-pars-cli/solutionFunctions.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ void computeSolutionFunctionsWithSparseEngine(std::shared_ptr<storm::models::spa
std::unique_ptr<storm::modelchecker::CheckResult> result =
storm::api::verifyWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true));
if (result) {
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult<ValueType>(model->getInitialStates()));
}
return result;
},
Expand Down
8 changes: 4 additions & 4 deletions src/storm-pars/derivative/SparseDerivativeInstantiationModelChecker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -143,20 +143,20 @@ void SparseDerivativeInstantiationModelChecker<FunctionType, ConstantType>::spec
if (this->currentFormula->isRewardOperatorFormula()) {
auto subformula = modelchecker::CheckTask<storm::logic::Formula, FunctionType>(
this->currentFormula->asRewardOperatorFormula().getSubformula().asEventuallyFormula().getSubformula());
target = propositionalChecker.check(subformula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
target = propositionalChecker.check(subformula)->template asExplicitQualitativeCheckResult<FunctionType>().getTruthValuesVector();
} else {
if (this->currentFormula->asProbabilityOperatorFormula().getSubformula().isUntilFormula()) {
auto rightSubformula = modelchecker::CheckTask<storm::logic::Formula, FunctionType>(
this->currentFormula->asProbabilityOperatorFormula().getSubformula().asUntilFormula().getRightSubformula());
auto leftSubformula = modelchecker::CheckTask<storm::logic::Formula, FunctionType>(
this->currentFormula->asProbabilityOperatorFormula().getSubformula().asUntilFormula().getLeftSubformula());
target = propositionalChecker.check(rightSubformula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
avoid = propositionalChecker.check(leftSubformula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
target = propositionalChecker.check(rightSubformula)->template asExplicitQualitativeCheckResult<FunctionType>().getTruthValuesVector();
avoid = propositionalChecker.check(leftSubformula)->template asExplicitQualitativeCheckResult<FunctionType>().getTruthValuesVector();
avoid.complement();
} else {
auto subformula = modelchecker::CheckTask<storm::logic::Formula, FunctionType>(
this->currentFormula->asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula());
target = propositionalChecker.check(subformula)->asExplicitQualitativeCheckResult().getTruthValuesVector();
target = propositionalChecker.check(subformula)->template asExplicitQualitativeCheckResult<FunctionType>().getTruthValuesVector();
}
}
initialStateModel = model.getStates("init").getNextSetIndex(0);
Expand Down
2 changes: 1 addition & 1 deletion src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -181,7 +181,7 @@ std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType
// Note that we can not consider the states with probability one since a state might reach a target state with prob 1 within >0 steps
std::unique_ptr<CheckResult> subFormulaResult =
modelChecker.check(env, this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula());
maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
maybeStates = maybeStates & ~(subFormulaResult->template asExplicitQualitativeCheckResult<ConstantType>().getTruthValuesVector());
hint.setMaybeStates(std::move(maybeStates));
hint.setComputeOnlyMaybeStates(true);
} else {
Expand Down
2 changes: 1 addition & 1 deletion src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -220,7 +220,7 @@ std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType,
// Note that we can not consider the states with probability one since a state might reach a target state with prob 1 within >0 steps
std::unique_ptr<CheckResult> subFormulaResult =
modelChecker.check(env, this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula());
maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
maybeStates = maybeStates & ~(subFormulaResult->template asExplicitQualitativeCheckResult<ConstantType>().getTruthValuesVector());
hint.setMaybeStates(std::move(maybeStates));
hint.setComputeOnlyMaybeStates(true);
} else {
Expand Down
25 changes: 15 additions & 10 deletions src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -150,10 +150,12 @@ void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType, Robus
STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) &&
propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()),
storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
storm::storage::BitVector phiStates =
std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
storm::storage::BitVector psiStates =
std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())
->template asExplicitQualitativeCheckResult<typename SparseModelType::ValueType>()
.getTruthValuesVector());
storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())
->template asExplicitQualitativeCheckResult<typename SparseModelType::ValueType>()
.getTruthValuesVector());

// get the maybeStates
maybeStates = storm::utility::graph::performProbGreater0(this->parametricModel->getBackwardTransitions(), phiStates, psiStates, true, *stepBound);
Expand Down Expand Up @@ -192,10 +194,12 @@ void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType, Robus
STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) &&
propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()),
storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
storm::storage::BitVector phiStates =
std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
storm::storage::BitVector psiStates =
std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())
->template asExplicitQualitativeCheckResult<typename SparseModelType::ValueType>()
.getTruthValuesVector());
storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())
->template asExplicitQualitativeCheckResult<typename SparseModelType::ValueType>()
.getTruthValuesVector());

// get the maybeStates
std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 =
Expand Down Expand Up @@ -264,8 +268,9 @@ void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType, Robus
storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(*this->parametricModel);
STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getSubformula()), storm::exceptions::NotSupportedException,
"Parameter lifting with non-propositional subformulas is not supported");
storm::storage::BitVector targetStates =
std::move(propositionalChecker.check(checkTask.getFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
storm::storage::BitVector targetStates = std::move(propositionalChecker.check(checkTask.getFormula().getSubformula())
->template asExplicitQualitativeCheckResult<typename SparseModelType::ValueType>()
.getTruthValuesVector());
// get the maybeStates
storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(
this->parametricModel->getBackwardTransitions(), storm::storage::BitVector(this->parametricModel->getNumberOfStates(), true), targetStates);
Expand Down
Loading