From c0dae886d1e8283a783ab884f64b443e436c106b Mon Sep 17 00:00:00 2001 From: Auto Format Date: Mon, 12 Aug 2024 11:03:19 +0000 Subject: [PATCH 1/2] Applied code formatting --- .../generator/DftNextStateGenerator.cpp | 11 +++++----- .../abstraction/MenuGameAbstractor.cpp | 6 ++---- src/storm-gspn/storage/gspn/GSPN.cpp | 6 ++---- src/storm-parsers/parser/SpiritErrorHandler.h | 3 +-- .../BeliefExplorationPomdpModelChecker.cpp | 7 +++---- ...processingPomdpValueBoundsModelChecker.cpp | 3 +-- src/storm/adapters/Smt2ExpressionAdapter.h | 4 +--- src/storm/automata/DeterministicAutomaton.cpp | 3 +-- .../automata/LTL2DeterministicAutomaton.cpp | 3 +-- src/storm/models/symbolic/Model.cpp | 3 +-- src/storm/storage/Scheduler.cpp | 4 ++-- src/storm/storage/SparseMatrix.cpp | 3 +-- src/storm/storage/jani/Model.cpp | 3 +-- src/storm/storage/prism/ClockVariable.cpp | 3 +-- src/storm/storage/prism/Constant.cpp | 3 +-- src/storm/storage/prism/HidingComposition.cpp | 4 +--- .../api/BeliefExplorationAPITest.cpp | 3 +-- ...BeliefExplorationPomdpModelCheckerTest.cpp | 21 +++++++------------ 18 files changed, 33 insertions(+), 60 deletions(-) diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 85fcc14766..a1dcbf822d 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -213,8 +213,8 @@ typename DftNextStateGenerator::DFTStatePointer DftNextSta if (dependencySuccessful) { // Dependency was successful -> dependent BE fails - STORM_LOG_TRACE("With the successful triggering of PDEP " << dependency->name() << " [" << dependency->id() << "]" - << " in " << mDft.getStateString(origState)); + STORM_LOG_TRACE("With the successful triggering of PDEP " << dependency->name() << " [" << dependency->id() << "]" << " in " + << mDft.getStateString(origState)); newState->letDependencyTrigger(dependency, true); STORM_LOG_ASSERT(dependency->dependentEvents().size() == 1, "Dependency " << dependency->name() << " does not have unique dependent event."); STORM_LOG_ASSERT(dependency->dependentEvents().front()->isBasicElement(), @@ -223,8 +223,8 @@ typename DftNextStateGenerator::DFTStatePointer DftNextSta return createSuccessorState(newState, trigger); } else { // Dependency was unsuccessful -> no BE fails - STORM_LOG_TRACE("With the unsuccessful triggering of PDEP " << dependency->name() << " [" << dependency->id() << "]" - << " in " << mDft.getStateString(origState)); + STORM_LOG_TRACE("With the unsuccessful triggering of PDEP " << dependency->name() << " [" << dependency->id() << "]" << " in " + << mDft.getStateString(origState)); newState->letDependencyTrigger(dependency, false); return newState; } @@ -236,8 +236,7 @@ typename DftNextStateGenerator::DFTStatePointer DftNextSta // Construct new state as copy from original one DFTStatePointer newState = origState->copy(); - STORM_LOG_TRACE("With the failure of " << be->name() << " [" << be->id() << "]" - << " in " << mDft.getStateString(origState)); + STORM_LOG_TRACE("With the failure of " << be->name() << " [" << be->id() << "]" << " in " << mDft.getStateString(origState)); newState->letBEFail(be); // Propagate diff --git a/src/storm-gamebased-ar/abstraction/MenuGameAbstractor.cpp b/src/storm-gamebased-ar/abstraction/MenuGameAbstractor.cpp index 9287d62a60..b0d283b9cb 100644 --- a/src/storm-gamebased-ar/abstraction/MenuGameAbstractor.cpp +++ b/src/storm-gamebased-ar/abstraction/MenuGameAbstractor.cpp @@ -140,8 +140,7 @@ void MenuGameAbstractor::exportToDot(storm::gbar::abstraction uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount()); out << stateName << "_" << index; out << " [ shape=\"square\", width=0, height=0, margin=0, label=\"" << index << "\" ];\n"; - out << "\tpl1_" << stateName << " -> " - << "pl2_" << stateName << "_" << index << " [ label=\"" << index << "\" ];\n"; + out << "\tpl1_" << stateName << " -> " << "pl2_" << stateName << "_" << index << " [ label=\"" << index << "\" ];\n"; } // Create the nodes of the probabilistic player. @@ -157,8 +156,7 @@ void MenuGameAbstractor::exportToDot(storm::gbar::abstraction index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame.getPlayer2Variables().size()); out << stateName << "_" << index; out << " [ shape=\"point\", label=\"\" ];\n"; - out << "\tpl2_" << stateName << " -> " - << "plp_" << stateName << "_" << index << " [ label=\"" << index << "\" ];\n"; + out << "\tpl2_" << stateName << " -> " << "plp_" << stateName << "_" << index << " [ label=\"" << index << "\" ];\n"; } for (auto stateValue : filteredTransitions) { diff --git a/src/storm-gspn/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp index 988b0257ac..8e414baacc 100644 --- a/src/storm-gspn/storage/gspn/GSPN.cpp +++ b/src/storm-gspn/storage/gspn/GSPN.cpp @@ -155,16 +155,14 @@ void GSPN::writeDotToStream(std::ostream& outStream) const { outStream << "digraph " << this->getName() << " {\n"; // print places with initial marking (not printed is the capacity) - outStream << "\t" - << "node [shape=ellipse]\n"; + outStream << "\t" << "node [shape=ellipse]\n"; for (auto& place : this->getPlaces()) { outStream << "\t" << place.getName() << " [label=\"" << place.getName() << "(" << place.getNumberOfInitialTokens(); outStream << ")\"];\n"; } // print transitions with weight/rate - outStream << "\t" - << "node [shape=box]\n"; + outStream << "\t" << "node [shape=box]\n"; for (auto& trans : this->getImmediateTransitions()) { outStream << "\t" << trans.getName() << " [fontcolor=white, style=filled, fillcolor=black, label=<" << trans.getName() diff --git a/src/storm-parsers/parser/SpiritErrorHandler.h b/src/storm-parsers/parser/SpiritErrorHandler.h index 6ea93ce5ff..d2eca180da 100644 --- a/src/storm-parsers/parser/SpiritErrorHandler.h +++ b/src/storm-parsers/parser/SpiritErrorHandler.h @@ -18,8 +18,7 @@ struct SpiritErrorHandler { std::string line(lineStart, lineEnd); std::stringstream stream; - stream << "Parsing error at " << get_line(where) << ":" << boost::spirit::get_column(lineStart, where) << ": " - << " expecting " << what << ", here:\n"; + stream << "Parsing error at " << get_line(where) << ":" << boost::spirit::get_column(lineStart, where) << ": " << " expecting " << what << ", here:\n"; stream << "\t" << line << '\n'; auto caretColumn = boost::spirit::get_column(lineStart, where); stream << "\t" << std::string(caretColumn - 1, ' ') << "^\n"; diff --git a/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.cpp b/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.cpp index 8fdfd8e81a..2dc5b31f5f 100644 --- a/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.cpp +++ b/src/storm-pomdp/modelchecker/BeliefExplorationPomdpModelChecker.cpp @@ -721,8 +721,7 @@ void BeliefExplorationPomdpModelChecker::UnfoldingControl::Pause && - !storm::utility::resources::isTerminate()) - ; + !storm::utility::resources::isTerminate()); } STORM_LOG_INFO("\tInteractive Unfolding terminated.\n"); } @@ -1090,8 +1089,8 @@ bool BeliefExplorationPomdpModelChecker= 60) { printUpdateStopwatch.restart(); - STORM_PRINT_AND_LOG("### " << underApproximation->getCurrentNumberOfMdpStates() << " beliefs in underapproximation MDP" - << " ##### " << underApproximation->getUnexploredStates().size() << " beliefs queued\n"); + STORM_PRINT_AND_LOG("### " << underApproximation->getCurrentNumberOfMdpStates() << " beliefs in underapproximation MDP" << " ##### " + << underApproximation->getUnexploredStates().size() << " beliefs queued\n"); if (underApproximation->getCurrentNumberOfMdpStates() > heuristicParameters.sizeThreshold && options.useClipping) { STORM_PRINT_AND_LOG("##### Clipping Attempts: " << statistics.nrClippingAttempts.value() << " ##### " << "Clipped States: " << statistics.nrClippedStates.value() << "\n"); diff --git a/src/storm-pomdp/modelchecker/PreprocessingPomdpValueBoundsModelChecker.cpp b/src/storm-pomdp/modelchecker/PreprocessingPomdpValueBoundsModelChecker.cpp index d678a5d86a..dbcf2b2cc7 100644 --- a/src/storm-pomdp/modelchecker/PreprocessingPomdpValueBoundsModelChecker.cpp +++ b/src/storm-pomdp/modelchecker/PreprocessingPomdpValueBoundsModelChecker.cpp @@ -18,8 +18,7 @@ namespace pomdp { namespace modelchecker { template PreprocessingPomdpValueBoundsModelChecker::PreprocessingPomdpValueBoundsModelChecker(storm::models::sparse::Pomdp const& pomdp) - : pomdp(pomdp) { /* Intentionally left empty */ -} + : pomdp(pomdp) { /* Intentionally left empty */ } template typename PreprocessingPomdpValueBoundsModelChecker::ValueBounds PreprocessingPomdpValueBoundsModelChecker::getValueBounds( diff --git a/src/storm/adapters/Smt2ExpressionAdapter.h b/src/storm/adapters/Smt2ExpressionAdapter.h index c5e49e1766..aa89d50527 100644 --- a/src/storm/adapters/Smt2ExpressionAdapter.h +++ b/src/storm/adapters/Smt2ExpressionAdapter.h @@ -61,9 +61,7 @@ class Smt2ExpressionAdapter { */ std::string translateExpression(storm::RationalFunction const& leftHandSide, storm::CompareRelation const& relation) { std::stringstream ss; - ss << "(" << relation << " " << leftHandSide.toString(false, useReadableVarNames) << " " - << "0 " - << ")"; + ss << "(" << relation << " " << leftHandSide.toString(false, useReadableVarNames) << " " << "0 " << ")"; return ss.str(); } diff --git a/src/storm/automata/DeterministicAutomaton.cpp b/src/storm/automata/DeterministicAutomaton.cpp index 5455b1b01d..d5922620ff 100644 --- a/src/storm/automata/DeterministicAutomaton.cpp +++ b/src/storm/automata/DeterministicAutomaton.cpp @@ -65,8 +65,7 @@ void DeterministicAutomaton::printHOA(std::ostream& out) const { out << "Acceptance: " << acceptance->getNumberOfAcceptanceSets() << " " << *acceptance->getAcceptanceExpression() << "\n"; - out << "--BODY--" - << "\n"; + out << "--BODY--" << "\n"; for (std::size_t s = 0; s < getNumberOfStates(); s++) { out << "State: " << s; diff --git a/src/storm/automata/LTL2DeterministicAutomaton.cpp b/src/storm/automata/LTL2DeterministicAutomaton.cpp index 048f0b89ef..b21b2f6f1c 100644 --- a/src/storm/automata/LTL2DeterministicAutomaton.cpp +++ b/src/storm/automata/LTL2DeterministicAutomaton.cpp @@ -79,8 +79,7 @@ std::shared_ptr LTL2DeterministicAutomaton::ltl2daExtern int status; // wait for completion - while (wait(&status) != pid) - ; + while (wait(&status) != pid); int rv; if (WIFEXITED(status)) { diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index f614ea6c31..09bed34cd7 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -375,8 +375,7 @@ void Model::printDdVariableInformationToStream(std::ostream& ou columnVariableCount += this->getManager().getMetaVariable(metaVariable).getNumberOfDdVariables(); } - out << "Variables: \t" - << "rows: " << this->rowVariables.size() << " meta variables (" << rowVariableCount << " DD variables)" + out << "Variables: \t" << "rows: " << this->rowVariables.size() << " meta variables (" << rowVariableCount << " DD variables)" << ", columns: " << this->columnVariables.size() << " meta variables (" << columnVariableCount << " DD variables)"; } diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index 84652762df..108f2b5f31 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/src/storm/storage/Scheduler.cpp @@ -191,8 +191,8 @@ void Scheduler::printToStream(std::ostream& out, std::shared_ptrgetTransitionMatrix().getRowGroupSize(state) == 1) { diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 6a67ead6b6..3c012646e2 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -386,8 +386,7 @@ void print(std::vector::index_type> const& rowG for (typename SparseMatrix::index_type i = rowGroupIndices[group]; i < endGroups; ++i) { endRows = i < rowIndications.size() - 1 ? rowIndications[i + 1] : columnsAndValues.size(); // Print the actual row. - std::cout << "Row " << i << " (" << rowIndications[i] << " - " << endRows << ")" - << ": "; + std::cout << "Row " << i << " (" << rowIndications[i] << " - " << endRows << ")" << ": "; for (typename SparseMatrix::index_type pos = rowIndications[i]; pos < endRows; ++pos) { std::cout << "(" << columnsAndValues[pos].getColumn() << ": " << columnsAndValues[pos].getValue() << ") "; } diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index e7ca22552a..d7e690b4b4 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -1631,8 +1631,7 @@ Model Model::createModelFromAutomaton(Automaton const& automaton) const { std::string filterName(std::string const& text) { std::string result = text; - std::replace_if( - result.begin(), result.end(), [](const char& c) { return std::ispunct(c); }, '_'); + std::replace_if(result.begin(), result.end(), [](const char& c) { return std::ispunct(c); }, '_'); return result; } diff --git a/src/storm/storage/prism/ClockVariable.cpp b/src/storm/storage/prism/ClockVariable.cpp index 47f988362d..7ed77fcd94 100644 --- a/src/storm/storage/prism/ClockVariable.cpp +++ b/src/storm/storage/prism/ClockVariable.cpp @@ -17,8 +17,7 @@ void ClockVariable::createMissingInitialValue() { } std::ostream& operator<<(std::ostream& stream, ClockVariable const& variable) { - stream << variable.getName() << ": clock" - << ";"; + stream << variable.getName() << ": clock" << ";"; return stream; } diff --git a/src/storm/storage/prism/Constant.cpp b/src/storm/storage/prism/Constant.cpp index f34e8509ca..48f6c8bfba 100644 --- a/src/storm/storage/prism/Constant.cpp +++ b/src/storm/storage/prism/Constant.cpp @@ -46,8 +46,7 @@ Constant Constant::substitute(std::map const& HidingComposition::getActionsToHide() const { } void HidingComposition::writeToStream(std::ostream& stream) const { - stream << "(" << *sub << ")" - << " " - << "{" << boost::join(actionsToHide, ", ") << "}"; + stream << "(" << *sub << ")" << " " << "{" << boost::join(actionsToHide, ", ") << "}"; } } // namespace prism diff --git a/src/test/storm-pomdp/api/BeliefExplorationAPITest.cpp b/src/test/storm-pomdp/api/BeliefExplorationAPITest.cpp index 42459173f6..b4b8cbd0bb 100644 --- a/src/test/storm-pomdp/api/BeliefExplorationAPITest.cpp +++ b/src/test/storm-pomdp/api/BeliefExplorationAPITest.cpp @@ -24,8 +24,7 @@ class DefaultDoubleVIEnvironment { static ValueType precision() { return storm::utility::convertNumber(0.12); } // there actually aren't any precision guarantees, but we still want to detect if results are weird. - static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions&) { /* intentionally left empty */ - } + static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions&) { /* intentionally left empty */ } }; template diff --git a/src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp b/src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp index 5c3ad7c916..078d336739 100644 --- a/src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp +++ b/src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp @@ -27,8 +27,7 @@ class DefaultDoubleVIEnvironment { static ValueType precision() { return storm::utility::convertNumber(0.12); } // there actually aren't any precision guarantees, but we still want to detect if results are weird. - static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions&) { /* intentionally left empty */ - } + static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions&) { /* intentionally left empty */ } static PreprocessingType const preprocessingType = PreprocessingType::None; }; @@ -45,8 +44,7 @@ class SelfloopReductionDefaultDoubleVIEnvironment { static ValueType precision() { return storm::utility::convertNumber(0.12); } // there actually aren't any precision guarantees, but we still want to detect if results are weird. - static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions&) { /* intentionally left empty */ - } + static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions&) { /* intentionally left empty */ } static PreprocessingType const preprocessingType = PreprocessingType::SelfloopReduction; }; @@ -63,8 +61,7 @@ class QualitativeReductionDefaultDoubleVIEnvironment { static ValueType precision() { return storm::utility::convertNumber(0.12); } // there actually aren't any precision guarantees, but we still want to detect if results are weird. - static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions&) { /* intentionally left empty */ - } + static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions&) { /* intentionally left empty */ } static PreprocessingType const preprocessingType = PreprocessingType::QualitativeReduction; }; @@ -81,8 +78,7 @@ class PreprocessedDefaultDoubleVIEnvironment { static ValueType precision() { return storm::utility::convertNumber(0.12); } // there actually aren't any precision guarantees, but we still want to detect if results are weird. - static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions&) { /* intentionally left empty */ - } + static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions&) { /* intentionally left empty */ } static PreprocessingType const preprocessingType = PreprocessingType::All; }; @@ -159,8 +155,7 @@ class DefaultDoubleOVIEnvironment { static ValueType precision() { return storm::utility::convertNumber(0.12); } // there actually aren't any precision guarantees, but we still want to detect if results are weird. - static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions&) { /* intentionally left empty */ - } + static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions&) { /* intentionally left empty */ } static PreprocessingType const preprocessingType = PreprocessingType::None; }; @@ -177,8 +172,7 @@ class DefaultRationalPIEnvironment { static ValueType precision() { return storm::utility::convertNumber(0.12); } // there actually aren't any precision guarantees, but we still want to detect if results are weird. - static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions&) { /* intentionally left empty */ - } + static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions&) { /* intentionally left empty */ } static PreprocessingType const preprocessingType = PreprocessingType::None; }; @@ -195,8 +189,7 @@ class PreprocessedDefaultRationalPIEnvironment { static ValueType precision() { return storm::utility::convertNumber(0.12); } // there actually aren't any precision guarantees, but we still want to detect if results are weird. - static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions&) { /* intentionally left empty */ - } + static void adaptOptions(storm::pomdp::modelchecker::BeliefExplorationPomdpModelCheckerOptions&) { /* intentionally left empty */ } static PreprocessingType const preprocessingType = PreprocessingType::All; }; From c6f5a0ff823ee538737b24f90ee84a259d0579b7 Mon Sep 17 00:00:00 2001 From: Auto Format Date: Mon, 12 Aug 2024 11:03:19 +0000 Subject: [PATCH 2/2] Add code formatting commit to .git-blame-ignore-revs --- .git-blame-ignore-revs | 1 + 1 file changed, 1 insertion(+) diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs index b20410928d..1c7d6d61de 100644 --- a/.git-blame-ignore-revs +++ b/.git-blame-ignore-revs @@ -13,3 +13,4 @@ e58679da05190fe064ca063b07ac56428162a8fb 634053fe63e39b80fff2355bb4e5b50839cd1e68 a177724097d3f807a6b8950b1cd378c34d040d1b 5016fac7d4014f1113c3d410a65aa5b39a74be64 +c0dae886d1e8283a783ab884f64b443e436c106b