diff --git a/src/adapters/GmmxxAdapter.h b/src/adapters/GmmxxAdapter.h
index 320e57021..df81b46f7 100644
--- a/src/adapters/GmmxxAdapter.h
+++ b/src/adapters/GmmxxAdapter.h
@@ -34,7 +34,7 @@ public:
template<class T>
static std::unique_ptr<gmm::csr_matrix<T>> toGmmxxSparseMatrix(storm::storage::SparseMatrix<T> const& matrix) {
uint_fast64_t realNonZeros = matrix.getEntryCount();
- LOG4CPLUS_DEBUG(logger, "Converting matrix with " << realNonZeros << " non-zeros to gmm++ format.");
+ STORM_LOG_DEBUG("Converting matrix with " << realNonZeros << " non-zeros to gmm++ format.");
// Prepare the resulting matrix.
std::unique_ptr<gmm::csr_matrix<T>> result(new gmm::csr_matrix<T>(matrix.getRowCount(), matrix.getColumnCount()));
@@ -58,7 +58,7 @@ public:
std::swap(result->ir, columns);
std::swap(result->pr, values);
- LOG4CPLUS_DEBUG(logger, "Done converting matrix to gmm++ format.");
+ STORM_LOG_DEBUG("Done converting matrix to gmm++ format.");
return result;
}
diff --git a/src/counterexamples/GenerateCounterexample.h b/src/counterexamples/GenerateCounterexample.h
index b111e16a8..f3b0e7ada 100644
--- a/src/counterexamples/GenerateCounterexample.h
+++ b/src/counterexamples/GenerateCounterexample.h
@@ -24,20 +24,20 @@
* @param parser An AutoParser to get the model from.
*/
void generateCounterExample(std::shared_ptr<storm::models::sparse::Model<double>> model) {
- LOG4CPLUS_INFO(logger, "Starting counterexample generation.");
- LOG4CPLUS_INFO(logger, "Testing inputs...");
+ STORM_LOG_INFO("Starting counterexample generation.");
+ STORM_LOG_INFO("Testing inputs...");
storm::settings::SettingsManager* s = storm::settings::SettingsManager::getInstance();
// First test output directory.
std::string outPath = s->getOptionByLongName("counterExample").getArgument(0).getValueAsString();
if(outPath.back() != '/' && outPath.back() != '\\') {
- LOG4CPLUS_ERROR(logger, "The output path is not valid.");
+ STORM_LOG_ERROR("The output path is not valid.");
return;
}
std::ofstream testFile(outPath + "test.dot");
if(testFile.fail()) {
- LOG4CPLUS_ERROR(logger, "The output path is not valid.");
+ STORM_LOG_ERROR("The output path is not valid.");
return;
}
testFile.close();
@@ -45,7 +45,7 @@
// Differentiate between model types.
if(model->getType() != storm::models::DTMC) {
- LOG4CPLUS_ERROR(logger, "Counterexample generation for the selected model type is not supported.");
+ STORM_LOG_ERROR("Counterexample generation for the selected model type is not supported.");
return;
}
@@ -53,21 +53,21 @@
// Note that the ownership of the object referenced by dtmc lies at the main function.
// Thus, it must not be deleted.
storm::models::Dtmc<double> dtmc = *(model->as<storm::models::Dtmc<double>>());
- LOG4CPLUS_INFO(logger, "Model is a DTMC.");
+ STORM_LOG_INFO("Model is a DTMC.");
// Get specified PRCTL formulas.
if(!s->isSet("prctl")) {
- LOG4CPLUS_ERROR(logger, "No PRCTL formula file specified.");
+ STORM_LOG_ERROR("No PRCTL formula file specified.");
return;
}
std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString();
- LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << ".");
+ STORM_LOG_INFO("Parsing prctl file: " << chosenPrctlFile << ".");
std::list<std::shared_ptr<storm::properties::prctl::PrctlFilter<double>>> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(chosenPrctlFile);
// Test for each formula if a counterexample can be generated for it.
if(formulaList.size() == 0) {
- LOG4CPLUS_ERROR(logger, "No PRCTL formula found.");
+ STORM_LOG_ERROR("No PRCTL formula found.");
return;
}
@@ -94,7 +94,7 @@
// First check if it is a formula type for which a counterexample can be generated.
if (std::dynamic_pointer_cast<storm::properties::prctl::AbstractStateFormula<double>>(formula->getChild()).get() == nullptr) {
- LOG4CPLUS_ERROR(logger, "Unexpected kind of formula. Expected a state formula.");
+ STORM_LOG_ERROR("Unexpected kind of formula. Expected a state formula.");
continue;
}
@@ -102,9 +102,9 @@
// Do some output
std::cout << "Generating counterexample for formula " << fIndex << ":" << std::endl;
- LOG4CPLUS_INFO(logger, "Generating counterexample for formula " + std::to_string(fIndex) + ": ");
+ STORM_LOG_INFO("Generating counterexample for formula " + std::to_string(fIndex) + ": ");
std::cout << "\t" << formula->toString() << "\n" << std::endl;
- LOG4CPLUS_INFO(logger, formula->toString());
+ STORM_LOG_INFO(formula->toString());
// Now check if the model does not satisfy the formula.
// That is if there is at least one initial state of the model that does not.
@@ -117,14 +117,14 @@
if((result & dtmc.getInitialStates()).getNumberOfSetBits() == dtmc.getInitialStates().getNumberOfSetBits()) {
std::cout << "Formula is satisfied. Can not generate counterexample.\n\n" << std::endl;
- LOG4CPLUS_INFO(logger, "Formula is satisfied. Can not generate counterexample.");
+ STORM_LOG_INFO("Formula is satisfied. Can not generate counterexample.");
continue;
}
// Generate counterexample
storm::models::Dtmc<double> counterExample = storm::counterexamples::PathBasedSubsystemGenerator<double>::computeCriticalSubsystem(dtmc, stateForm);
- LOG4CPLUS_INFO(logger, "Found counterexample.");
+ STORM_LOG_INFO("Found counterexample.");
// Output counterexample
// Do standard output
diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h
index 87f02c668..ffc398e34 100644
--- a/src/counterexamples/MILPMinimalLabelSetGenerator.h
+++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h
@@ -98,10 +98,10 @@ namespace storm {
result.relevantStates &= ~psiStates;
result.problematicStates = storm::utility::graph::performProb0E(labeledMdp.getTransitionMatrix(), labeledMdp.getNondeterministicChoiceIndices(), labeledMdp.getBackwardTransitions(), phiStates, psiStates);
result.problematicStates &= result.relevantStates;
- LOG4CPLUS_DEBUG(logger, "Found " << phiStates.getNumberOfSetBits() << " filter states.");
- LOG4CPLUS_DEBUG(logger, "Found " << psiStates.getNumberOfSetBits() << " target states.");
- LOG4CPLUS_DEBUG(logger, "Found " << result.relevantStates.getNumberOfSetBits() << " relevant states.");
- LOG4CPLUS_DEBUG(logger, "Found " << result.problematicStates.getNumberOfSetBits() << " problematic states.");
+ STORM_LOG_DEBUG("Found " << phiStates.getNumberOfSetBits() << " filter states.");
+ STORM_LOG_DEBUG("Found " << psiStates.getNumberOfSetBits() << " target states.");
+ STORM_LOG_DEBUG("Found " << result.relevantStates.getNumberOfSetBits() << " relevant states.");
+ STORM_LOG_DEBUG("Found " << result.problematicStates.getNumberOfSetBits() << " problematic states.");
return result;
}
@@ -158,7 +158,7 @@ namespace storm {
// Finally, determine the set of labels that are known to be taken.
result.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(labeledMdp, psiStates, result.allRelevantLabels);
- LOG4CPLUS_DEBUG(logger, "Found " << result.allRelevantLabels.size() << " relevant labels and " << result.knownLabels.size() << " known labels.");
+ STORM_LOG_DEBUG("Found " << result.allRelevantLabels.size() << " relevant labels and " << result.knownLabels.size() << " known labels.");
return result;
}
@@ -364,47 +364,47 @@ namespace storm {
std::pair<std::unordered_map<uint_fast64_t, storm::expressions::Variable>, uint_fast64_t> labelVariableResult = createLabelVariables(solver, choiceInformation.allRelevantLabels);
result.labelToVariableMap = std::move(labelVariableResult.first);
result.numberOfVariables += labelVariableResult.second;
- LOG4CPLUS_DEBUG(logger, "Created variables for labels.");
+ STORM_LOG_DEBUG("Created variables for labels.");
// Create scheduler variables for relevant states and their actions.
std::pair<std::unordered_map<uint_fast64_t, std::list<storm::expressions::Variable>>, uint_fast64_t> schedulerVariableResult = createSchedulerVariables(solver, stateInformation, choiceInformation);
result.stateToChoiceVariablesMap = std::move(schedulerVariableResult.first);
result.numberOfVariables += schedulerVariableResult.second;
- LOG4CPLUS_DEBUG(logger, "Created variables for nondeterministic choices.");
+ STORM_LOG_DEBUG("Created variables for nondeterministic choices.");
// Create scheduler variables for nondeterministically choosing an initial state.
std::pair<std::unordered_map<uint_fast64_t, storm::expressions::Variable>, uint_fast64_t> initialChoiceVariableResult = createInitialChoiceVariables(solver, labeledMdp, stateInformation);
result.initialStateToChoiceVariableMap = std::move(initialChoiceVariableResult.first);
result.numberOfVariables += initialChoiceVariableResult.second;
- LOG4CPLUS_DEBUG(logger, "Created variables for the nondeterministic choice of the initial state.");
+ STORM_LOG_DEBUG("Created variables for the nondeterministic choice of the initial state.");
// Create variables for probabilities for all relevant states.
std::pair<std::unordered_map<uint_fast64_t, storm::expressions::Variable>, uint_fast64_t> probabilityVariableResult = createProbabilityVariables(solver, stateInformation);
result.stateToProbabilityVariableMap = std::move(probabilityVariableResult.first);
result.numberOfVariables += probabilityVariableResult.second;
- LOG4CPLUS_DEBUG(logger, "Created variables for the reachability probabilities.");
+ STORM_LOG_DEBUG("Created variables for the reachability probabilities.");
// Create a probability variable for a virtual initial state that nondeterministically chooses one of the system's real initial states as its target state.
std::pair<storm::expressions::Variable, uint_fast64_t> virtualInitialStateVariableResult = createVirtualInitialStateVariable(solver);
result.virtualInitialStateVariable = virtualInitialStateVariableResult.first;
result.numberOfVariables += virtualInitialStateVariableResult.second;
- LOG4CPLUS_DEBUG(logger, "Created variables for the virtual initial state.");
+ STORM_LOG_DEBUG("Created variables for the virtual initial state.");
// Create variables for problematic states.
std::pair<std::unordered_map<uint_fast64_t, storm::expressions::Variable>, uint_fast64_t> problematicStateVariableResult = createProblematicStateVariables(solver, labeledMdp, stateInformation, choiceInformation);
result.problematicStateToVariableMap = std::move(problematicStateVariableResult.first);
result.numberOfVariables += problematicStateVariableResult.second;
- LOG4CPLUS_DEBUG(logger, "Created variables for the problematic states.");
+ STORM_LOG_DEBUG("Created variables for the problematic states.");
// Create variables for problematic choices.
std::pair<std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable, PairHash>, uint_fast64_t> problematicTransitionVariableResult = createProblematicChoiceVariables(solver, labeledMdp, stateInformation, choiceInformation);
result.problematicTransitionToVariableMap = problematicTransitionVariableResult.first;
result.numberOfVariables += problematicTransitionVariableResult.second;
- LOG4CPLUS_DEBUG(logger, "Created variables for the problematic choices.");
+ STORM_LOG_DEBUG("Created variables for the problematic choices.");
// Finally, we need to update the model to make the new variables usable.
solver.update();
- LOG4CPLUS_INFO(logger, "Successfully created " << result.numberOfVariables << " MILP variables.");
+ STORM_LOG_INFO("Successfully created " << result.numberOfVariables << " MILP variables.");
// Finally, return variable information struct.
return result;
@@ -816,43 +816,43 @@ namespace storm {
static void buildConstraintSystem(storm::solver::LpSolver& solver, storm::models::sparse::Mdp<T> const& labeledMdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound, bool includeSchedulerCuts = false) {
// Assert that the reachability probability in the subsystem exceeds the given threshold.
uint_fast64_t numberOfConstraints = assertProbabilityGreaterThanThreshold(solver, labeledMdp, variableInformation, probabilityThreshold, strictBound);
- LOG4CPLUS_DEBUG(logger, "Asserted that reachability probability exceeds threshold.");
+ STORM_LOG_DEBUG("Asserted that reachability probability exceeds threshold.");
// Add constraints that assert the policy takes at most one action in each state.
numberOfConstraints += assertValidPolicy(solver, stateInformation, variableInformation);
- LOG4CPLUS_DEBUG(logger, "Asserted that policy is valid.");
+ STORM_LOG_DEBUG("Asserted that policy is valid.");
// Add constraints that assert the labels that belong to some taken choices are taken as well.
numberOfConstraints += assertChoicesImplyLabels(solver, labeledMdp, stateInformation, choiceInformation, variableInformation);
- LOG4CPLUS_DEBUG(logger, "Asserted that labels implied by choices are taken.");
+ STORM_LOG_DEBUG("Asserted that labels implied by choices are taken.");
// Add constraints that encode that the reachability probability from states which do not pick any action
// is zero.
numberOfConstraints += assertZeroProbabilityWithoutChoice(solver, stateInformation, choiceInformation, variableInformation);
- LOG4CPLUS_DEBUG(logger, "Asserted that reachability probability is zero if no choice is taken.");
+ STORM_LOG_DEBUG("Asserted that reachability probability is zero if no choice is taken.");
// Add constraints that encode the reachability probabilities for states.
numberOfConstraints += assertReachabilityProbabilities(solver, labeledMdp, psiStates, stateInformation, choiceInformation, variableInformation);
- LOG4CPLUS_DEBUG(logger, "Asserted constraints for reachability probabilities.");
+ STORM_LOG_DEBUG("Asserted constraints for reachability probabilities.");
// Add constraints that ensure the reachability of an unproblematic state from each problematic state.
numberOfConstraints += assertUnproblematicStateReachable(solver, labeledMdp, stateInformation, choiceInformation, variableInformation);
- LOG4CPLUS_DEBUG(logger, "Asserted that unproblematic state reachable from problematic states.");
+ STORM_LOG_DEBUG("Asserted that unproblematic state reachable from problematic states.");
// Add constraints that express that certain labels are already known to be taken.
numberOfConstraints += assertKnownLabels(solver, labeledMdp, psiStates, choiceInformation, variableInformation);
- LOG4CPLUS_DEBUG(logger, "Asserted known labels are taken.");
+ STORM_LOG_DEBUG("Asserted known labels are taken.");
// If required, assert additional constraints that reduce the number of possible policies.
if (includeSchedulerCuts) {
numberOfConstraints += assertSchedulerCuts(solver, labeledMdp, psiStates, stateInformation, choiceInformation, variableInformation);
- LOG4CPLUS_DEBUG(logger, "Asserted scheduler cuts.");
+ STORM_LOG_DEBUG("Asserted scheduler cuts.");
}
// Finally, we can tell the solver to incorporate the latest changes.
solver.update();
- LOG4CPLUS_INFO(logger, "Successfully created " << numberOfConstraints << " MILP constraints.");
+ STORM_LOG_INFO("Successfully created " << numberOfConstraints << " MILP constraints.");
}
/*!
diff --git a/src/counterexamples/PathBasedSubsystemGenerator.h b/src/counterexamples/PathBasedSubsystemGenerator.h
index 465ee5608..6061e9449 100644
--- a/src/counterexamples/PathBasedSubsystemGenerator.h
+++ b/src/counterexamples/PathBasedSubsystemGenerator.h
@@ -100,7 +100,7 @@ public:
}
}
- LOG4CPLUS_DEBUG(logger, "Initialized.");
+ STORM_LOG_DEBUG("Initialized.");
//Now find the shortest distances to all states
while(!activeSet.empty()) {
@@ -151,7 +151,7 @@ public:
}
}
- LOG4CPLUS_DEBUG(logger, "Discovery done.");
+ STORM_LOG_DEBUG("Discovery done.");
}
/*!
@@ -215,7 +215,7 @@ public:
}
}
- LOG4CPLUS_DEBUG(logger, "Initialized.");
+ STORM_LOG_DEBUG("Initialized.");
//Now find the shortest distances to all states
while(!activeSet.empty()) {
@@ -269,7 +269,7 @@ public:
}
}
- LOG4CPLUS_DEBUG(logger, "Discovery done.");
+ STORM_LOG_DEBUG("Discovery done.");
}
/*!
@@ -324,7 +324,7 @@ public:
if(distances[bestIndex].second == (T) -1){
shortestPath.push_back(bestIndex);
probability = (T) 0;
- LOG4CPLUS_DEBUG(logger, "Terminal state not viable!");
+ STORM_LOG_DEBUG("Terminal state not viable!");
return;
}
@@ -338,8 +338,8 @@ public:
bestIndex = distances[bestIndex].first;
}
- LOG4CPLUS_DEBUG(logger, "Found best state: " << bestIndex);
- LOG4CPLUS_DEBUG(logger, "Value: " << bestValue);
+ STORM_LOG_DEBUG("Found best state: " << bestIndex);
+ STORM_LOG_DEBUG("Value: " << bestValue);
shortestPath.push_back(bestIndex);
bestIndex = distances[bestIndex].first;
@@ -382,9 +382,9 @@ public:
//-------------------------------------------------------------
#ifdef BENCHMARK
- LOG4CPLUS_INFO(logger, "Formula: " << stateFormula.toString());
+ STORM_LOG_INFO("Formula: " << stateFormula.toString());
#endif
- LOG4CPLUS_INFO(logger, "Start finding critical subsystem.");
+ STORM_LOG_INFO("Start finding critical subsystem.");
// make model checker
// TODO: Implement and use generic Model Checker factory.
@@ -397,7 +397,7 @@ public:
std::shared_ptr<storm::properties::prctl::ProbabilisticBoundOperator<T>> boundOperator = std::dynamic_pointer_cast<storm::properties::prctl::ProbabilisticBoundOperator<T>>(stateFormula);
if(boundOperator == nullptr){
- LOG4CPLUS_ERROR(logger, "No path bound operator at formula root.");
+ STORM_LOG_ERROR("No path bound operator at formula root.");
return model.getSubDtmc(subSys);
}
T bound = boundOperator->getBound();
@@ -440,7 +440,7 @@ public:
targetStates = until->getRight()->check(modelCheck);
}
else {
- LOG4CPLUS_ERROR(logger, "Strange path formula. Can't decipher.");
+ STORM_LOG_ERROR("Strange path formula. Can't decipher.");
return model.getSubDtmc(subSys);
}
@@ -476,11 +476,11 @@ public:
if((initStates & targetStates).getNumberOfSetBits() != 0) {
subSys.set(*(initStates & targetStates).begin());
- LOG4CPLUS_INFO(logger, "Critical subsystem found.");
- LOG4CPLUS_INFO(logger, "Paths needed: " << pathCount);
- LOG4CPLUS_INFO(logger, "State count of critical subsystem: " << subSys.getNumberOfSetBits());
- LOG4CPLUS_INFO(logger, "Prob: " << 1);
- LOG4CPLUS_INFO(logger, "Model checks: " << mcCount);
+ STORM_LOG_INFO("Critical subsystem found.");
+ STORM_LOG_INFO("Paths needed: " << pathCount);
+ STORM_LOG_INFO("State count of critical subsystem: " << subSys.getNumberOfSetBits());
+ STORM_LOG_INFO("Prob: " << 1);
+ STORM_LOG_INFO("Model checks: " << mcCount);
return model.getSubDtmc(subSys);
}
@@ -555,11 +555,11 @@ public:
}
}
- LOG4CPLUS_INFO(logger, "Critical subsystem found.");
- LOG4CPLUS_INFO(logger, "Paths needed: " << pathCount);
- LOG4CPLUS_INFO(logger, "State count of critical subsystem: " << subSys.getNumberOfSetBits());
- LOG4CPLUS_INFO(logger, "Prob: " << subSysProb);
- LOG4CPLUS_INFO(logger, "Model checks: " << mcCount);
+ STORM_LOG_INFO("Critical subsystem found.");
+ STORM_LOG_INFO("Paths needed: " << pathCount);
+ STORM_LOG_INFO("State count of critical subsystem: " << subSys.getNumberOfSetBits());
+ STORM_LOG_INFO("Prob: " << subSysProb);
+ STORM_LOG_INFO("Model checks: " << mcCount);
return model.getSubDtmc(subSys);
}
diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h
index 3f03440d3..f7a2704b5 100644
--- a/src/counterexamples/SMTMinimalCommandSetGenerator.h
+++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h
@@ -99,8 +99,8 @@ namespace storm {
relevancyInformation.relevantStates = storm::utility::graph::performProbGreater0E(labeledMdp.getTransitionMatrix(), labeledMdp.getNondeterministicChoiceIndices(), backwardTransitions, phiStates, psiStates);
relevancyInformation.relevantStates &= ~psiStates;
- LOG4CPLUS_DEBUG(logger, "Found " << relevancyInformation.relevantStates.getNumberOfSetBits() << " relevant states.");
- LOG4CPLUS_DEBUG(logger, relevancyInformation.relevantStates);
+ STORM_LOG_DEBUG("Found " << relevancyInformation.relevantStates.getNumberOfSetBits() << " relevant states.");
+ STORM_LOG_DEBUG(relevancyInformation.relevantStates);
// Retrieve some references for convenient access.
storm::storage::SparseMatrix<T> const& transitionMatrix = labeledMdp.getTransitionMatrix();
@@ -141,7 +141,7 @@ namespace storm {
std::cout << "Found " << relevancyInformation.relevantLabels.size() << " relevant and " << relevancyInformation.knownLabels.size() << " known labels." << std::endl;
- LOG4CPLUS_DEBUG(logger, "Found " << relevancyInformation.relevantLabels.size() << " relevant and " << relevancyInformation.knownLabels.size() << " known labels.");
+ STORM_LOG_DEBUG("Found " << relevancyInformation.relevantLabels.size() << " relevant and " << relevancyInformation.knownLabels.size() << " known labels.");
return relevancyInformation;
}
@@ -350,9 +350,9 @@ namespace storm {
}
}
- LOG4CPLUS_DEBUG(logger, "Successfully gathered data for explicit cuts.");
+ STORM_LOG_DEBUG("Successfully gathered data for explicit cuts.");
- LOG4CPLUS_DEBUG(logger, "Asserting initial combination is taken.");
+ STORM_LOG_DEBUG("Asserting initial combination is taken.");
{
std::vector<storm::expressions::Expression> formulae;
@@ -378,7 +378,7 @@ namespace storm {
}
}
- LOG4CPLUS_DEBUG(logger, "Asserting target combination is taken.");
+ STORM_LOG_DEBUG("Asserting target combination is taken.");
{
std::vector<storm::expressions::Expression> formulae;
@@ -414,7 +414,7 @@ namespace storm {
}
}
- LOG4CPLUS_DEBUG(logger, "Asserting taken labels are followed by another label if they are not a target label.");
+ STORM_LOG_DEBUG("Asserting taken labels are followed by another label if they are not a target label.");
// Now assert that for each non-target label, we take a following label.
for (auto const& labelSetFollowingSetsPair : followingLabels) {
std::vector<storm::expressions::Expression> formulae;
@@ -502,7 +502,7 @@ namespace storm {
}
}
- LOG4CPLUS_DEBUG(logger, "Asserting synchronization cuts.");
+ STORM_LOG_DEBUG("Asserting synchronization cuts.");
// Finally, assert that if we take one of the synchronizing labels, we also take one of the combinations
// the label appears in.
for (auto const& labelSynchronizingSetsPair : synchronizingLabels) {
@@ -667,7 +667,7 @@ namespace storm {
// If the solver reports unsat, then we know that the current selection is not enabled in the initial state.
if (checkResult == storm::solver::SmtSolver::CheckResult::Unsat) {
- LOG4CPLUS_DEBUG(logger, "Selection not enabled in initial state.");
+ STORM_LOG_DEBUG("Selection not enabled in initial state.");
storm::expressions::Expression guardConjunction;
if (currentCommandVector.size() == 1) {
guardConjunction = currentCommandVector.begin()->get().getGuardExpression();
@@ -685,10 +685,10 @@ namespace storm {
}
} else {
throw storm::exceptions::InvalidStateException() << "Choice label set is empty.";
- LOG4CPLUS_DEBUG(logger, "Choice label set is empty.");
+ STORM_LOG_DEBUG("Choice label set is empty.");
}
- LOG4CPLUS_DEBUG(logger, "About to assert disjunction of negated guards.");
+ STORM_LOG_DEBUG("About to assert disjunction of negated guards.");
storm::expressions::Expression guardExpression = localManager.boolean(false);
bool firstAssignment = true;
for (auto const& command : currentCommandVector) {
@@ -699,7 +699,7 @@ namespace storm {
}
}
localSolver->add(guardExpression);
- LOG4CPLUS_DEBUG(logger, "Asserted disjunction of negated guards.");
+ STORM_LOG_DEBUG("Asserted disjunction of negated guards.");
// Now check the possible preceding label sets for the essential ones.
for (auto const& precedingLabelSet : labelSetAndPrecedingLabelSetsPair.second) {
@@ -742,10 +742,10 @@ namespace storm {
}
}
- LOG4CPLUS_DEBUG(logger, "About to assert a weakest precondition.");
+ STORM_LOG_DEBUG("About to assert a weakest precondition.");
storm::expressions::Expression wp = guardConjunction.substitute(currentUpdateCombinationMap);
formulae.push_back(wp);
- LOG4CPLUS_DEBUG(logger, "Asserted weakest precondition.");
+ STORM_LOG_DEBUG("Asserted weakest precondition.");
// Now try to move iterators to the next position if possible. If we could properly move it, we can directly
// move on to the next combination of updates. If we have to reset it to the start, we
@@ -768,7 +768,7 @@ namespace storm {
// Now assert the disjunction of all weakest preconditions of all considered update combinations.
assertDisjunction(*localSolver, formulae, localManager);
- LOG4CPLUS_DEBUG(logger, "Asserted disjunction of all weakest preconditions.");
+ STORM_LOG_DEBUG("Asserted disjunction of all weakest preconditions.");
if (localSolver->check() == storm::solver::SmtSolver::CheckResult::Sat) {
backwardImplications[labelSetAndPrecedingLabelSetsPair.first].insert(precedingLabelSet);
@@ -793,7 +793,7 @@ namespace storm {
}
}
- LOG4CPLUS_DEBUG(logger, "Asserting taken labels are preceded by another label if they are not an initial label.");
+ STORM_LOG_DEBUG("Asserting taken labels are preceded by another label if they are not an initial label.");
// Now assert that for each non-target label, we take a following label.
for (auto const& labelSetImplicationsPair : backwardImplications) {
std::vector<storm::expressions::Expression> formulae;
@@ -1042,7 +1042,7 @@ namespace storm {
static std::vector<storm::expressions::Expression> createAdder(VariableInformation const& variableInformation, std::vector<storm::expressions::Expression> const& in1, std::vector<storm::expressions::Expression> const& in2) {
// Sanity check for sizes of input.
if (in1.size() != in2.size() || in1.size() == 0) {
- LOG4CPLUS_ERROR(logger, "Illegal input to adder (" << in1.size() << ", " << in2.size() << ").");
+ STORM_LOG_ERROR("Illegal input to adder (" << in1.size() << ", " << in2.size() << ").");
throw storm::exceptions::InvalidArgumentException() << "Illegal input to adder.";
}
@@ -1097,7 +1097,7 @@ namespace storm {
* @return A bit vector representing the number of literals that are set to true.
*/
static std::vector<storm::expressions::Expression> createCounterCircuit(VariableInformation const& variableInformation, std::vector<storm::expressions::Variable> const& literals) {
- LOG4CPLUS_DEBUG(logger, "Creating counter circuit for " << literals.size() << " literals.");
+ STORM_LOG_DEBUG("Creating counter circuit for " << literals.size() << " literals.");
// Create the auxiliary vector.
std::vector<std::vector<storm::expressions::Expression>> aux;
@@ -1136,7 +1136,7 @@ namespace storm {
* @return The relaxation variable associated with the constraint.
*/
static storm::expressions::Variable assertLessOrEqualKRelaxed(storm::solver::SmtSolver& solver, VariableInformation const& variableInformation, uint64_t k) {
- LOG4CPLUS_DEBUG(logger, "Asserting solution has size less or equal " << k << ".");
+ STORM_LOG_DEBUG("Asserting solution has size less or equal " << k << ".");
std::vector<storm::expressions::Variable> const& input = variableInformation.adderVariables;
@@ -1209,16 +1209,16 @@ namespace storm {
}
// Check whether the assumptions are satisfiable.
- LOG4CPLUS_DEBUG(logger, "Invoking satisfiability checking.");
+ STORM_LOG_DEBUG("Invoking satisfiability checking.");
z3::check_result result = solver.check(assumptions);
- LOG4CPLUS_DEBUG(logger, "Done invoking satisfiability checking.");
+ STORM_LOG_DEBUG("Done invoking satisfiability checking.");
if (result == z3::sat) {
return true;
} else {
- LOG4CPLUS_DEBUG(logger, "Computing unsat core.");
+ STORM_LOG_DEBUG("Computing unsat core.");
z3::expr_vector unsatCore = solver.unsat_core();
- LOG4CPLUS_DEBUG(logger, "Computed unsat core.");
+ STORM_LOG_DEBUG("Computed unsat core.");
std::vector<z3::expr> blockingVariables;
blockingVariables.reserve(unsatCore.size());
@@ -1334,7 +1334,7 @@ namespace storm {
// As long as the constraints are unsatisfiable, we need to relax the last at-most-k constraint and
// try with an increased bound.
while (solver.checkWithAssumptions({assumption}) == storm::solver::SmtSolver::CheckResult::Unsat) {
- LOG4CPLUS_DEBUG(logger, "Constraint system is unsatisfiable with at most " << currentBound << " taken commands; increasing bound.");
+ STORM_LOG_DEBUG("Constraint system is unsatisfiable with at most " << currentBound << " taken commands; increasing bound.");
solver.add(variableInformation.auxiliaryVariables.back());
variableInformation.auxiliaryVariables.push_back(assertLessOrEqualKRelaxed(solver, variableInformation, ++currentBound));
assumption = !variableInformation.auxiliaryVariables.back();
@@ -1359,7 +1359,7 @@ namespace storm {
static void analyzeZeroProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::sparse::Mdp<T> const& subMdp, storm::models::sparse::Mdp<T> const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set<uint_fast64_t> const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) {
storm::storage::BitVector reachableStates(subMdp.getNumberOfStates());
- LOG4CPLUS_DEBUG(logger, "Analyzing solution with zero probability.");
+ STORM_LOG_DEBUG("Analyzing solution with zero probability.");
// Initialize the stack for the DFS.
bool targetStateIsReachable = false;
@@ -1403,10 +1403,10 @@ namespace storm {
}
}
- LOG4CPLUS_DEBUG(logger, "Successfully performed reachability analysis.");
+ STORM_LOG_DEBUG("Successfully performed reachability analysis.");
if (targetStateIsReachable) {
- LOG4CPLUS_ERROR(logger, "Target must be unreachable for this analysis.");
+ STORM_LOG_ERROR("Target must be unreachable for this analysis.");
throw storm::exceptions::InvalidStateException() << "Target must be unreachable for this analysis.";
}
@@ -1417,7 +1417,7 @@ namespace storm {
std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin()));
std::vector<boost::container::flat_set<uint_fast64_t>> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, statesThatCanReachTargetStates, locallyRelevantLabels);
- LOG4CPLUS_DEBUG(logger, "Found " << reachableLabels.size() << " reachable labels and " << reachableStates.getNumberOfSetBits() << " reachable states.");
+ STORM_LOG_DEBUG("Found " << reachableLabels.size() << " reachable labels and " << reachableStates.getNumberOfSetBits() << " reachable states.");
// Search for states on the border of the reachable state space, i.e. states that are still reachable
// and possess a (disabled) option to leave the reachable part of the state space.
@@ -1466,7 +1466,7 @@ namespace storm {
formulae.push_back(cube);
}
- LOG4CPLUS_DEBUG(logger, "Asserting reachability implications.");
+ STORM_LOG_DEBUG("Asserting reachability implications.");
assertDisjunction(solver, formulae, *variableInformation.manager);
}
@@ -1484,7 +1484,7 @@ namespace storm {
*/
static void analyzeInsufficientProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::sparse::Mdp<T> const& subMdp, storm::models::sparse::Mdp<T> const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set<uint_fast64_t> const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) {
- LOG4CPLUS_DEBUG(logger, "Analyzing solution with insufficient probability.");
+ STORM_LOG_DEBUG("Analyzing solution with insufficient probability.");
storm::storage::BitVector reachableStates(subMdp.getNumberOfStates());
@@ -1529,7 +1529,7 @@ namespace storm {
}
}
}
- LOG4CPLUS_DEBUG(logger, "Successfully determined reachable state space.");
+ STORM_LOG_DEBUG("Successfully determined reachable state space.");
storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates;
storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp.getTransitionMatrix(), subMdp.getNondeterministicChoiceIndices(), subMdp.getBackwardTransitions(), phiStates, psiStates);
@@ -1574,7 +1574,7 @@ namespace storm {
formulae.push_back(cube);
}
- LOG4CPLUS_DEBUG(logger, "Asserting reachability implications.");
+ STORM_LOG_DEBUG("Asserting reachability implications.");
assertDisjunction(solver, formulae, *variableInformation.manager);
}
#endif
@@ -1627,7 +1627,7 @@ namespace storm {
double maximalReachabilityProbability = 0;
if (checkThresholdFeasible) {
storm::modelchecker::helper::SparseMdpPrctlHelper<T> modelCheckerHelper;
- LOG4CPLUS_DEBUG(logger, "Invoking model checker.");
+ STORM_LOG_DEBUG("Invoking model checker.");
std::vector<T> result = std::move(modelCheckerHelper.computeUntilProbabilities(false, labeledMdp.getTransitionMatrix(), labeledMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::utility::solver::MinMaxLinearEquationSolverFactory<T>()).values);
for (auto state : labeledMdp.getInitialStates()) {
maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]);
@@ -1645,7 +1645,7 @@ namespace storm {
// (4) Create the variables for the relevant commands.
VariableInformation variableInformation = createVariables(manager, labeledMdp, psiStates, relevancyInformation, includeReachabilityEncoding);
- LOG4CPLUS_DEBUG(logger, "Created variables.");
+ STORM_LOG_DEBUG("Created variables.");
// (5) Now assert an adder whose result variables can later be used to constrain the nummber of label
// variables that were set to true. Initially, we are looking for a solution that has no label enabled
@@ -1654,14 +1654,14 @@ namespace storm {
variableInformation.auxiliaryVariables.push_back(assertLessOrEqualKRelaxed(*solver, variableInformation, 0));
// (6) Add constraints that cut off a lot of suboptimal solutions.
- LOG4CPLUS_DEBUG(logger, "Asserting cuts.");
+ STORM_LOG_DEBUG("Asserting cuts.");
assertExplicitCuts(labeledMdp, psiStates, variableInformation, relevancyInformation, *solver);
- LOG4CPLUS_DEBUG(logger, "Asserted explicit cuts.");
+ STORM_LOG_DEBUG("Asserted explicit cuts.");
assertSymbolicCuts(preparedProgram, labeledMdp, variableInformation, relevancyInformation, *solver);
- LOG4CPLUS_DEBUG(logger, "Asserted symbolic cuts.");
+ STORM_LOG_DEBUG("Asserted symbolic cuts.");
if (includeReachabilityEncoding) {
assertReachabilityCuts(labeledMdp, psiStates, variableInformation, relevancyInformation, *solver);
- LOG4CPLUS_DEBUG(logger, "Asserted reachability cuts.");
+ STORM_LOG_DEBUG("Asserted reachability cuts.");
}
// As we are done with the setup at this point, stop the clock for the setup time.
@@ -1680,20 +1680,20 @@ namespace storm {
maximalReachabilityProbability = 0;
uint_fast64_t zeroProbabilityCount = 0;
do {
- LOG4CPLUS_DEBUG(logger, "Computing minimal command set.");
+ STORM_LOG_DEBUG("Computing minimal command set.");
solverClock = std::chrono::high_resolution_clock::now();
commandSet = findSmallestCommandSet(*solver, variableInformation, currentBound);
totalSolverTime += std::chrono::high_resolution_clock::now() - solverClock;
- LOG4CPLUS_DEBUG(logger, "Computed minimal command set of size " << (commandSet.size() + relevancyInformation.knownLabels.size()) << ".");
+ STORM_LOG_DEBUG("Computed minimal command set of size " << (commandSet.size() + relevancyInformation.knownLabels.size()) << ".");
// Restrict the given MDP to the current set of labels and compute the reachability probability.
modelCheckingClock = std::chrono::high_resolution_clock::now();
commandSet.insert(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end());
storm::models::sparse::Mdp<T> subMdp = labeledMdp.restrictChoiceLabels(commandSet);
storm::modelchecker::helper::SparseMdpPrctlHelper<T> modelCheckerHelper;
- LOG4CPLUS_DEBUG(logger, "Invoking model checker.");
+ STORM_LOG_DEBUG("Invoking model checker.");
std::vector<T> result = std::move(modelCheckerHelper.computeUntilProbabilities(false, subMdp.getTransitionMatrix(), subMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::utility::solver::MinMaxLinearEquationSolverFactory<T>()).values);
- LOG4CPLUS_DEBUG(logger, "Computed model checking results.");
+ STORM_LOG_DEBUG("Computed model checking results.");
totalModelCheckingTime += std::chrono::high_resolution_clock::now() - modelCheckingClock;
// Now determine the maximal reachability probability by checking all initial states.
diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
index adec586dd..09cac3521 100644
--- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
@@ -87,9 +87,9 @@ namespace storm {
storm::storage::BitVector statesWithProbability0 = std::move(statesWithProbability01.first);
storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second);
storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
- LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
- LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
- LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
+ STORM_LOG_INFO("Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
+ STORM_LOG_INFO("Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
+ STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
// Create resulting vector.
std::vector<ValueType> result(transitionMatrix.getRowGroupCount());
@@ -287,16 +287,16 @@ namespace storm {
}
infinityStates.complement();
storm::storage::BitVector maybeStates = ~targetStates & ~infinityStates;
- LOG4CPLUS_INFO(logger, "Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states.");
- LOG4CPLUS_INFO(logger, "Found " << targetStates.getNumberOfSetBits() << " 'target' states.");
- LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
+ STORM_LOG_INFO("Found " << infinityStates.getNumberOfSetBits() << " 'infinity' states.");
+ STORM_LOG_INFO("Found " << targetStates.getNumberOfSetBits() << " 'target' states.");
+ STORM_LOG_INFO("Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
// Create resulting vector.
std::vector<ValueType> result(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
// Check whether we need to compute exact rewards for some states.
if (qualitative) {
- LOG4CPLUS_INFO(logger, "The rewards for the initial states were determined in a preprocessing step. No exact rewards were computed.");
+ STORM_LOG_INFO("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
// are neither 0 nor infinity.
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, storm::utility::one<ValueType>());
diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp
index 31c222207..cbfeed391 100644
--- a/src/models/sparse/Dtmc.cpp
+++ b/src/models/sparse/Dtmc.cpp
@@ -33,7 +33,7 @@ namespace storm {
//
// // Is there any state in the subsystem?
// if(subSysStates.getNumberOfSetBits() == 0) {
- // LOG4CPLUS_ERROR(logger, "No states in subsystem!");
+ // STORM_LOG_ERROR("No states in subsystem!");
// return storm::models::Dtmc<ValueType>(storm::storage::SparseMatrix<ValueType>(),
// storm::models::sparse::StateLabeling(this->getStateLabeling(), subSysStates),
// boost::optional<std::vector<ValueType>>(),
@@ -43,13 +43,13 @@ namespace storm {
//
// // Does the vector have the right size?
// if(subSysStates.size() != this->getNumberOfStates()) {
- // LOG4CPLUS_INFO(logger, "BitVector has wrong size. Resizing it...");
+ // STORM_LOG_INFO("BitVector has wrong size. Resizing it...");
// subSysStates.resize(this->getNumberOfStates());
// }
//
// // Test if it is a proper subsystem of this Dtmc, i.e. if there is at least one state to be left out.
// if(subSysStates.getNumberOfSetBits() == subSysStates.size()) {
- // LOG4CPLUS_INFO(logger, "All states are kept. This is no proper subsystem.");
+ // STORM_LOG_INFO("All states are kept. This is no proper subsystem.");
// return storm::models::Dtmc<ValueType>(*this);
// }
//
diff --git a/src/parser/AtomicPropositionLabelingParser.cpp b/src/parser/AtomicPropositionLabelingParser.cpp
index 8e51fb305..349bfb56b 100644
--- a/src/parser/AtomicPropositionLabelingParser.cpp
+++ b/src/parser/AtomicPropositionLabelingParser.cpp
@@ -29,7 +29,7 @@ namespace storm {
// Open the given file.
if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": The supplied Labeling input file does not exist or is not readable by this process.");
+ STORM_LOG_ERROR("Error while parsing " << filename << ": The supplied Labeling input file does not exist or is not readable by this process.");
throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": The supplied Labeling input file does not exist or is not readable by this process.";
}
@@ -68,9 +68,9 @@ namespace storm {
// If #DECLARATION or #END have not been found, the file format is wrong.
if (!(foundDecl && foundEnd)) {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File header is corrupted (#DECLARATION or #END missing - case sensitive).");
- if (!foundDecl) LOG4CPLUS_ERROR(logger, "\tDid not find #DECLARATION token.");
- if (!foundEnd) LOG4CPLUS_ERROR(logger, "\tDid not find #END token.");
+ STORM_LOG_ERROR("Error while parsing " << filename << ": File header is corrupted (#DECLARATION or #END missing - case sensitive).");
+ if (!foundDecl) STORM_LOG_ERROR("\tDid not find #DECLARATION token.");
+ if (!foundEnd) STORM_LOG_ERROR("\tDid not find #END token.");
throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": File header is corrupted (#DECLARATION or #END missing - case sensitive).";
}
@@ -99,7 +99,7 @@ namespace storm {
if (cnt >= sizeof(proposition)) {
// if token is longer than our buffer, the following strncpy code might get risky...
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": Atomic proposition with length > " << (sizeof(proposition) - 1) << " was found.");
+ 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) {
@@ -138,7 +138,7 @@ namespace storm {
// 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) {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously.");
+ 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.";
}
@@ -159,7 +159,7 @@ namespace storm {
// Has the label been declared in the header?
if(!labeling.containsLabel(proposition)) {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": Atomic proposition" << proposition << " was found but not declared.");
+ 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.";
}
labeling.addLabelToState(proposition, state);
diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp
index 2ec30fb64..6f3c60c46 100644
--- a/src/parser/AutoParser.cpp
+++ b/src/parser/AutoParser.cpp
@@ -54,7 +54,7 @@ namespace storm {
break;
}
default:
- LOG4CPLUS_WARN(logger, "Unknown/Unhandled Model Type which cannot be parsed."); // Unknown
+ STORM_LOG_WARN("Unknown/Unhandled Model Type which cannot be parsed."); // Unknown
}
return model;
diff --git a/src/parser/DeterministicSparseTransitionParser.cpp b/src/parser/DeterministicSparseTransitionParser.cpp
index 94b82a4c7..f18b46441 100644
--- a/src/parser/DeterministicSparseTransitionParser.cpp
+++ b/src/parser/DeterministicSparseTransitionParser.cpp
@@ -46,7 +46,7 @@ namespace storm {
setlocale(LC_NUMERIC, "C");
if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
+ STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable.");
throw storm::exceptions::FileIoException() << "The supplied Transition input file \"" << filename << "\" does not exist or is not readable by this process.";
}
@@ -58,11 +58,11 @@ namespace storm {
bool insertDiagonalEntriesIfMissing = !isRewardFile;
DeterministicSparseTransitionParser<ValueType>::FirstPassResult firstPass = DeterministicSparseTransitionParser<ValueType>::firstPass(file.getData(), insertDiagonalEntriesIfMissing);
- LOG4CPLUS_INFO(logger, "First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " NonZeros.");
+ STORM_LOG_INFO("First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " NonZeros.");
// If first pass returned zero, the file format was wrong.
if (firstPass.numberOfNonzeroEntries == 0) {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": empty or erroneous file format.");
+ STORM_LOG_ERROR("Error while parsing " << filename << ": empty or erroneous file format.");
throw storm::exceptions::WrongFormatException();
}
@@ -78,7 +78,7 @@ namespace storm {
if (isRewardFile) {
// The reward matrix should match the size of the transition matrix.
if (firstPass.highestStateIndex + 1 > transitionMatrix.getRowCount() || firstPass.highestStateIndex + 1 > transitionMatrix.getColumnCount()) {
- LOG4CPLUS_ERROR(logger, "Reward matrix has more rows or columns than transition matrix.");
+ STORM_LOG_ERROR("Reward matrix has more rows or columns than transition matrix.");
throw storm::exceptions::WrongFormatException() << "Reward matrix has more rows or columns than transition matrix.";
} else {
// If we found the right number of states or less, we set it to the number of states represented by the transition matrix.
@@ -122,9 +122,9 @@ namespace storm {
hadDeadlocks = true;
if (!dontFixDeadlocks) {
resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::one<ValueType>());
- LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted.");
+ STORM_LOG_WARN("Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted.");
} else {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions.");
+ STORM_LOG_ERROR("Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions.");
// Before throwing the appropriate exception we will give notice of all deadlock states.
}
}
@@ -143,9 +143,9 @@ namespace storm {
if (!rowHadDiagonalEntry) {
if (insertDiagonalEntriesIfMissing) {
resultMatrix.addNextValue(lastRow, lastRow, storm::utility::zero<ValueType>());
- LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)");
+ STORM_LOG_DEBUG("While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)");
} else {
- LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
+ STORM_LOG_WARN("Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
}
// No increment for lastRow.
rowHadDiagonalEntry = true;
@@ -154,9 +154,9 @@ namespace storm {
hadDeadlocks = true;
if (!dontFixDeadlocks) {
resultMatrix.addNextValue(skippedRow, skippedRow, storm::utility::one<ValueType>());
- LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted.");
+ STORM_LOG_WARN("Warning while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions. A self-loop was inserted.");
} else {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions.");
+ STORM_LOG_ERROR("Error while parsing " << filename << ": state " << skippedRow << " has no outgoing transitions.");
// Before throwing the appropriate exception we will give notice of all deadlock states.
}
}
@@ -171,9 +171,9 @@ namespace storm {
if (col > row && !rowHadDiagonalEntry) {
if (insertDiagonalEntriesIfMissing) {
resultMatrix.addNextValue(row, row, storm::utility::zero<ValueType>());
- LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)");
+ STORM_LOG_DEBUG("While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)");
} else {
- LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << row << " has no transition to itself.");
+ STORM_LOG_WARN("Warning while parsing " << filename << ": state " << row << " has no transition to itself.");
}
rowHadDiagonalEntry = true;
}
@@ -185,9 +185,9 @@ namespace storm {
if (!rowHadDiagonalEntry) {
if (insertDiagonalEntriesIfMissing) {
resultMatrix.addNextValue(lastRow, lastRow, storm::utility::zero<ValueType>());
- LOG4CPLUS_DEBUG(logger, "While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)");
+ STORM_LOG_DEBUG("While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)");
} else {
- LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
+ STORM_LOG_WARN("Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself.");
}
}
@@ -200,7 +200,7 @@ namespace storm {
// Since we cannot check if each transition for which there is a reward in the reward file also exists in the transition matrix during parsing, we have to do it afterwards.
if (isRewardFile && !result.isSubmatrixOf(transitionMatrix)) {
- LOG4CPLUS_ERROR(logger, "There are rewards for non existent transitions given in the reward file.");
+ STORM_LOG_ERROR("There are rewards for non existent transitions given in the reward file.");
throw storm::exceptions::WrongFormatException() << "There are rewards for non existent transitions given in the reward file.";
}
@@ -272,7 +272,7 @@ namespace storm {
// Have we already seen this transition?
if (row == lastRow && col == lastCol) {
- LOG4CPLUS_ERROR(logger, "The same transition (" << row << ", " << col << ") is given twice.");
+ STORM_LOG_ERROR("The same transition (" << row << ", " << col << ") is given twice.");
throw storm::exceptions::InvalidArgumentException() << "The same transition (" << row << ", " << col << ") is given twice.";
}
diff --git a/src/parser/MappedFile.cpp b/src/parser/MappedFile.cpp
index 7abf526cf..86f2648eb 100644
--- a/src/parser/MappedFile.cpp
+++ b/src/parser/MappedFile.cpp
@@ -33,20 +33,20 @@ namespace storm {
#else
if (stat64(filename, &(this->st)) != 0) {
#endif
- LOG4CPLUS_ERROR(logger, "Error in stat(" << filename << "): Probably, this file does not exist.");
+ STORM_LOG_ERROR("Error in stat(" << filename << "): Probably, this file does not exist.");
throw exceptions::FileIoException() << "MappedFile Error in stat(): Probably, this file does not exist.";
}
this->file = open(filename, O_RDONLY);
if (this->file < 0) {
- LOG4CPLUS_ERROR(logger, "Error in open(" << filename << "): Probably, we may not read this file.");
+ STORM_LOG_ERROR("Error in open(" << filename << "): Probably, we may not read this file.");
throw exceptions::FileIoException() << "MappedFile Error in open(): Probably, we may not read this file.";
}
this->data = static_cast<char*>(mmap(NULL, this->st.st_size, PROT_READ, MAP_PRIVATE, this->file, 0));
if (this->data == MAP_FAILED) {
close(this->file);
- LOG4CPLUS_ERROR(logger, "Error in mmap(" << filename << "): " << std::strerror(errno));
+ STORM_LOG_ERROR("Error in mmap(" << filename << "): " << std::strerror(errno));
throw exceptions::FileIoException() << "MappedFile Error in mmap(): " << std::strerror(errno);
}
this->dataEnd = this->data + this->st.st_size;
@@ -56,20 +56,20 @@ namespace storm {
// _stat64(), CreateFile(), CreateFileMapping(), MapViewOfFile()
if (_stat64(filename, &(this->st)) != 0) {
- LOG4CPLUS_ERROR(logger, "Error in _stat(" << filename << "): Probably, this file does not exist.");
+ STORM_LOG_ERROR("Error in _stat(" << filename << "): Probably, this file does not exist.");
throw exceptions::FileIoException("MappedFile Error in stat(): Probably, this file does not exist.");
}
this->file = CreateFileA(filename, GENERIC_READ, 0, NULL, OPEN_ALWAYS, FILE_ATTRIBUTE_NORMAL, NULL);
if (this->file == INVALID_HANDLE_VALUE) {
- LOG4CPLUS_ERROR(logger, "Error in CreateFileA(" << filename << "): Probably, we may not read this file.");
+ STORM_LOG_ERROR("Error in CreateFileA(" << filename << "): Probably, we may not read this file.");
throw exceptions::FileIoException("MappedFile Error in CreateFileA(): Probably, we may not read this file.");
}
this->mapping = CreateFileMappingA(this->file, NULL, PAGE_READONLY, (DWORD)(st.st_size >> 32), (DWORD)st.st_size, NULL);
if (this->mapping == NULL) {
CloseHandle(this->file);
- LOG4CPLUS_ERROR(logger, "Error in CreateFileMappingA(" << filename << ").");
+ STORM_LOG_ERROR("Error in CreateFileMappingA(" << filename << ").");
throw exceptions::FileIoException("MappedFile Error in CreateFileMappingA().");
}
@@ -77,7 +77,7 @@ namespace storm {
if (this->data == NULL) {
CloseHandle(this->mapping);
CloseHandle(this->file);
- LOG4CPLUS_ERROR(logger, "Error in MapViewOfFile(" << filename << ").");
+ STORM_LOG_ERROR("Error in MapViewOfFile(" << filename << ").");
throw exceptions::FileIoException("MappedFile Error in MapViewOfFile().");
}
this->dataEnd = this->data + this->st.st_size;
diff --git a/src/parser/MarkovAutomatonParser.cpp b/src/parser/MarkovAutomatonParser.cpp
index 6a68abda8..b4ee7be34 100644
--- a/src/parser/MarkovAutomatonParser.cpp
+++ b/src/parser/MarkovAutomatonParser.cpp
@@ -37,7 +37,7 @@ namespace storm {
// Since Markov Automata do not support transition rewards no path should be given here.
if (transitionRewardFilename != "") {
- LOG4CPLUS_ERROR(logger, "Transition rewards are unsupported for Markov automata.");
+ STORM_LOG_ERROR("Transition rewards are unsupported for Markov automata.");
throw storm::exceptions::WrongFormatException() << "Transition rewards are unsupported for Markov automata.";
}
diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp
index 6bc214cab..18d87d314 100644
--- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp
+++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp
@@ -48,11 +48,11 @@ namespace storm {
result.numberOfNonzeroEntries += source - lastsource - 1;
result.numberOfChoices += source - lastsource - 1;
} else {
- LOG4CPLUS_ERROR(logger, "Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag.");
+ STORM_LOG_ERROR("Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag.");
throw storm::exceptions::WrongFormatException() << "Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag.";
}
} else if (source < lastsource) {
- LOG4CPLUS_ERROR(logger, "Illegal state choice order. A choice of state " << source << " appears at an illegal position.");
+ STORM_LOG_ERROR("Illegal state choice order. A choice of state " << source << " appears at an illegal position.");
throw storm::exceptions::WrongFormatException() << "Illegal state choice order. A choice of state " << source << " appears at an illegal position.";
}
@@ -80,11 +80,11 @@ namespace storm {
if (isMarkovianChoice) {
if (stateHasMarkovianChoice) {
- LOG4CPLUS_ERROR(logger, "The state " << source << " has multiple Markovian choices.");
+ STORM_LOG_ERROR("The state " << source << " has multiple Markovian choices.");
throw storm::exceptions::WrongFormatException() << "The state " << source << " has multiple Markovian choices.";
}
if (stateHasProbabilisticChoice) {
- LOG4CPLUS_ERROR(logger, "The state " << source << " has a probabilistic choice preceding a Markovian choice. The Markovian choice must be the first choice listed.");
+ STORM_LOG_ERROR("The state " << source << " has a probabilistic choice preceding a Markovian choice. The Markovian choice must be the first choice listed.");
throw storm::exceptions::WrongFormatException() << "The state " << source << " has a probabilistic choice preceding a Markovian choice. The Markovian choice must be the first choice listed.";
}
stateHasMarkovianChoice = true;
@@ -106,7 +106,7 @@ namespace storm {
// If the end of the file was reached, we need to abort and check whether we are in a legal state.
if (buf[0] == '\0') {
if (!hasSuccessorState) {
- LOG4CPLUS_ERROR(logger, "Premature end-of-file. Expected at least one successor state for state " << source << ".");
+ STORM_LOG_ERROR("Premature end-of-file. Expected at least one successor state for state " << source << ".");
throw storm::exceptions::WrongFormatException() << "Premature end-of-file. Expected at least one successor state for state " << source << ".";
} else {
// If there was at least one successor for the current choice, this is legal and we need to move on.
@@ -122,18 +122,18 @@ namespace storm {
result.highestStateIndex = target;
}
if (hasSuccessorState && target <= lastSuccessorState) {
- LOG4CPLUS_ERROR(logger, "Illegal transition order for source state " << source << ".");
+ STORM_LOG_ERROR("Illegal transition order for source state " << source << ".");
throw storm::exceptions::WrongFormatException() << "Illegal transition order for source state " << source << ".";
}
// And the corresponding probability/rate.
double val = checked_strtod(buf, &buf);
if (val < 0.0) {
- LOG4CPLUS_ERROR(logger, "Illegal negative probability/rate value for transition from " << source << " to " << target << ": " << val << ".");
+ STORM_LOG_ERROR("Illegal negative probability/rate value for transition from " << source << " to " << target << ": " << val << ".");
throw storm::exceptions::WrongFormatException() << "Illegal negative probability/rate value for transition from " << source << " to " << target << ": " << val << ".";
}
if (!isMarkovianChoice && val > 1.0) {
- LOG4CPLUS_ERROR(logger, "Illegal probability value for transition from " << source << " to " << target << ": " << val << ".");
+ STORM_LOG_ERROR("Illegal probability value for transition from " << source << " to " << target << ": " << val << ".");
throw storm::exceptions::WrongFormatException() << "Illegal probability value for transition from " << source << " to " << target << ": " << val << ".";
}
@@ -191,7 +191,7 @@ namespace storm {
++currentChoice;
}
} else {
- LOG4CPLUS_ERROR(logger, "Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag.");
+ STORM_LOG_ERROR("Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag.");
throw storm::exceptions::WrongFormatException() << "Found deadlock states (e.g. " << lastsource + 1 << ") during parsing. Please fix them or set the appropriate flag.";
}
}
@@ -269,7 +269,7 @@ namespace storm {
setlocale(LC_NUMERIC, "C");
if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
+ STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable.");
throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": File does not exist or is not readable.";
}
diff --git a/src/parser/NondeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp
index 421f3b8cc..89322808c 100644
--- a/src/parser/NondeterministicSparseTransitionParser.cpp
+++ b/src/parser/NondeterministicSparseTransitionParser.cpp
@@ -44,7 +44,7 @@ namespace storm {
setlocale(LC_NUMERIC, "C");
if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
+ STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable.");
throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": File does not exist or is not readable.";
}
@@ -57,7 +57,7 @@ namespace storm {
// If first pass returned zero, the file format was wrong.
if (firstPass.numberOfNonzeroEntries == 0) {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": erroneous file format.");
+ STORM_LOG_ERROR("Error while parsing " << filename << ": erroneous file format.");
throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": erroneous file format.";
}
@@ -73,13 +73,13 @@ namespace storm {
if (isRewardFile) {
// The reward matrix should match the size of the transition matrix.
if (firstPass.choices > modelInformation.getRowCount() || (uint_fast64_t) (firstPass.highestStateIndex + 1) > modelInformation.getColumnCount()) {
- LOG4CPLUS_ERROR(logger, "Reward matrix size exceeds transition matrix size.");
+ STORM_LOG_ERROR("Reward matrix size exceeds transition matrix size.");
throw storm::exceptions::OutOfRangeException() << "Reward matrix size exceeds transition matrix size.";
} else if (firstPass.choices != modelInformation.getRowCount()) {
- LOG4CPLUS_ERROR(logger, "Reward matrix row count does not match transition matrix row count.");
+ STORM_LOG_ERROR("Reward matrix row count does not match transition matrix row count.");
throw storm::exceptions::OutOfRangeException() << "Reward matrix row count does not match transition matrix row count.";
} else if (firstPass.numberOfNonzeroEntries > modelInformation.getEntryCount()) {
- LOG4CPLUS_ERROR(logger, "The reward matrix has more entries than the transition matrix. There must be a reward for a non existent transition");
+ STORM_LOG_ERROR("The reward matrix has more entries than the transition matrix. There must be a reward for a non existent transition");
throw storm::exceptions::OutOfRangeException() << "The reward matrix has more entries than the transition matrix.";
} else {
firstPass.highestStateIndex = modelInformation.getColumnCount() - 1;
@@ -89,7 +89,7 @@ namespace storm {
// Create the matrix builder.
// The matrix to be build should have as many columns as we have nodes and as many rows as we have choices.
// Those two values, as well as the number of nonzero elements, was been calculated in the first run.
- LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << firstPass.choices << " x " << (firstPass.highestStateIndex + 1) << " with " << firstPass.numberOfNonzeroEntries << " entries.");
+ STORM_LOG_INFO("Attempting to create matrix of size " << firstPass.choices << " x " << (firstPass.highestStateIndex + 1) << " with " << firstPass.numberOfNonzeroEntries << " entries.");
storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
if (!isRewardFile) {
matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(firstPass.choices, firstPass.highestStateIndex + 1, firstPass.numberOfNonzeroEntries, true, true, firstPass.highestStateIndex + 1);
@@ -155,9 +155,9 @@ namespace storm {
matrixBuilder.newRowGroup(curRow);
matrixBuilder.addNextValue(curRow, node, 1);
++curRow;
- LOG4CPLUS_WARN(logger, "Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
+ STORM_LOG_WARN("Warning while parsing " << filename << ": node " << node << " has no outgoing transitions. A self-loop was inserted.");
} else {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": node " << node << " has no outgoing transitions.");
+ STORM_LOG_ERROR("Error while parsing " << filename << ": node " << node << " has no outgoing transitions.");
}
}
if (source != lastSource) {
@@ -194,7 +194,7 @@ namespace storm {
// Since we cannot check if each transition for which there is a reward in the reward file also exists in the transition matrix during parsing, we have to do it afterwards.
if (isRewardFile && !resultMatrix.isSubmatrixOf(modelInformation)) {
- LOG4CPLUS_ERROR(logger, "There are rewards for non existent transitions given in the reward file.");
+ STORM_LOG_ERROR("There are rewards for non existent transitions given in the reward file.");
throw storm::exceptions::WrongFormatException() << "There are rewards for non existent transitions given in the reward file.";
}
@@ -230,7 +230,7 @@ namespace storm {
choice = checked_strtol(buf, &buf);
if (source < lastSource) {
- LOG4CPLUS_ERROR(logger, "The current source state " << source << " is smaller than the last one " << lastSource << ".");
+ STORM_LOG_ERROR("The current source state " << source << " is smaller than the last one " << lastSource << ".");
throw storm::exceptions::InvalidArgumentException() << "The current source state " << source << " is smaller than the last one " << lastSource << ".";
}
@@ -243,7 +243,7 @@ namespace storm {
// Make sure that the highest state index of the reward file is not higher than the highest state index of the corresponding model.
if (result.highestStateIndex > modelInformation.getColumnCount() - 1) {
- LOG4CPLUS_ERROR(logger, "State index " << result.highestStateIndex << " found. This exceeds the highest state index of the model, which is " << modelInformation.getColumnCount() - 1 << " .");
+ STORM_LOG_ERROR("State index " << result.highestStateIndex << " found. This exceeds the highest state index of the model, which is " << modelInformation.getColumnCount() - 1 << " .");
throw storm::exceptions::OutOfRangeException() << "State index " << result.highestStateIndex << " found. This exceeds the highest state index of the model, which is " << modelInformation.getColumnCount() - 1 << " .";
}
@@ -292,18 +292,18 @@ namespace storm {
// Also, have we already seen this transition?
if (target == lastTarget && choice == lastChoice && source == lastSource) {
- LOG4CPLUS_ERROR(logger, "The same transition (" << source << ", " << choice << ", " << target << ") is given twice.");
+ STORM_LOG_ERROR("The same transition (" << source << ", " << choice << ", " << target << ") is given twice.");
throw storm::exceptions::InvalidArgumentException() << "The same transition (" << source << ", " << choice << ", " << target << ") is given twice.";
}
// Read value and check whether it's positive.
val = checked_strtod(buf, &buf);
if (!isRewardFile && (val < 0.0 || val > 1.0)) {
- LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << std::string(buf, 0, 16) << "\".");
+ STORM_LOG_ERROR("Expected a positive probability but got \"" << std::string(buf, 0, 16) << "\".");
NondeterministicSparseTransitionParser::FirstPassResult nullResult;
return nullResult;
} else if (val < 0.0) {
- LOG4CPLUS_ERROR(logger, "Expected a positive reward value but got \"" << std::string(buf, 0, 16) << "\".");
+ STORM_LOG_ERROR("Expected a positive reward value but got \"" << std::string(buf, 0, 16) << "\".");
NondeterministicSparseTransitionParser::FirstPassResult nullResult;
return nullResult;
}
diff --git a/src/parser/SparseChoiceLabelingParser.cpp b/src/parser/SparseChoiceLabelingParser.cpp
index 7bfeeb459..999a98841 100644
--- a/src/parser/SparseChoiceLabelingParser.cpp
+++ b/src/parser/SparseChoiceLabelingParser.cpp
@@ -14,7 +14,7 @@ namespace storm {
std::vector<storm::models::sparse::LabelSet> SparseChoiceLabelingParser::parseChoiceLabeling(std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, std::string const& filename) {
// Open file.
if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
+ STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable.");
throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": File does not exist or is not readable.";
}
diff --git a/src/parser/SparseStateRewardParser.cpp b/src/parser/SparseStateRewardParser.cpp
index b60856eb8..35e1c3d59 100644
--- a/src/parser/SparseStateRewardParser.cpp
+++ b/src/parser/SparseStateRewardParser.cpp
@@ -22,7 +22,7 @@ namespace storm {
std::vector<ValueType> SparseStateRewardParser<ValueType>::parseSparseStateReward(uint_fast64_t stateCount, std::string const& filename) {
// Open file.
if (!MappedFile::fileExistsAndIsReadable(filename.c_str())) {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": File does not exist or is not readable.");
+ STORM_LOG_ERROR("Error while parsing " << filename << ": File does not exist or is not readable.");
throw storm::exceptions::FileIoException() << "Error while parsing " << filename << ": File does not exist or is not readable.";
}
@@ -47,12 +47,12 @@ namespace storm {
// If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks).
// Note: The value -1 shows that lastState has not yet been set, i.e. this is the first run of the loop (state index (2^64)-1 is a really bad starting index).
if (state <= lastState && lastState != startIndexComparison) {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": State " << state << " was found but has already been read or skipped previously.");
+ 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.";
}
if (stateCount <= state) {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": Found reward for a state of an invalid index \"" << state << "\". The model has only " << stateCount << " states.");
+ STORM_LOG_ERROR("Error while parsing " << filename << ": Found reward for a state of an invalid index \"" << state << "\". The model has only " << stateCount << " states.");
throw storm::exceptions::OutOfRangeException() << "Error while parsing " << filename << ": Found reward for a state of an invalid index \"" << state << "\"";
}
@@ -60,7 +60,7 @@ namespace storm {
reward = checked_strtod(buf, &buf);
if (reward < 0.0) {
- LOG4CPLUS_ERROR(logger, "Error while parsing " << filename << ": Expected positive reward value but got \"" << reward << "\".");
+ STORM_LOG_ERROR("Error while parsing " << filename << ": Expected positive reward value but got \"" << reward << "\".");
throw storm::exceptions::WrongFormatException() << "Error while parsing " << filename << ": State reward file specifies illegal reward value.";
}
diff --git a/src/solver/GmmxxLinearEquationSolver.cpp b/src/solver/GmmxxLinearEquationSolver.cpp
index 3b7bbf476..eb869481c 100644
--- a/src/solver/GmmxxLinearEquationSolver.cpp
+++ b/src/solver/GmmxxLinearEquationSolver.cpp
@@ -56,9 +56,9 @@ namespace storm {
template<typename ValueType>
void GmmxxLinearEquationSolver<ValueType>::solveEquationSystem(std::vector<ValueType>& x, std::vector<ValueType> const& b, std::vector<ValueType>* multiplyResult) const {
- LOG4CPLUS_INFO(logger, "Using method '" << methodToString() << "' with preconditioner '" << preconditionerToString() << "' (max. " << maximalNumberOfIterations << " iterations).");
+ STORM_LOG_INFO("Using method '" << methodToString() << "' with preconditioner '" << preconditionerToString() << "' (max. " << maximalNumberOfIterations << " iterations).");
if (method == SolutionMethod::Jacobi && preconditioner != Preconditioner::None) {
- LOG4CPLUS_WARN(logger, "Jacobi method currently does not support preconditioners. The requested preconditioner will be ignored.");
+ STORM_LOG_WARN("Jacobi method currently does not support preconditioners. The requested preconditioner will be ignored.");
}
if (method == SolutionMethod::Bicgstab || method == SolutionMethod::Qmr || method == SolutionMethod::Gmres) {
@@ -93,18 +93,18 @@ namespace storm {
// Check if the solver converged and issue a warning otherwise.
if (iter.converged()) {
- LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iter.get_iteration() << " iterations.");
+ STORM_LOG_INFO("Iterative solver converged after " << iter.get_iteration() << " iterations.");
} else {
- LOG4CPLUS_WARN(logger, "Iterative solver did not converge.");
+ STORM_LOG_WARN("Iterative solver did not converge.");
}
} else if (method == SolutionMethod::Jacobi) {
uint_fast64_t iterations = solveLinearEquationSystemWithJacobi(*originalA, x, b, multiplyResult);
// Check if the solver converged and issue a warning otherwise.
if (iterations < maximalNumberOfIterations) {
- LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterations << " iterations.");
+ STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations.");
} else {
- LOG4CPLUS_WARN(logger, "Iterative solver did not converge.");
+ STORM_LOG_WARN("Iterative solver did not converge.");
}
}
}
diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp
index 07052e6eb..eed6fb258 100644
--- a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp
+++ b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp
@@ -69,9 +69,9 @@ namespace storm {
// Check if the solver converged and issue a warning otherwise.
if (converged) {
- LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterations << " iterations.");
+ STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations.");
} else {
- LOG4CPLUS_WARN(logger, "Iterative solver did not converge after " << iterations << " iterations.");
+ STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations.");
}
// If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result
@@ -149,9 +149,9 @@ namespace storm {
// Check if the solver converged and issue a warning otherwise.
if (converged) {
- LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterations << " iterations.");
+ STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations.");
} else {
- LOG4CPLUS_WARN(logger, "Iterative solver did not converge after " << iterations << " iterations.");
+ STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations.");
}
// If requested, we store the scheduler for retrieval.
diff --git a/src/solver/GurobiLpSolver.cpp b/src/solver/GurobiLpSolver.cpp
index 202aa6e45..4108f2bb8 100644
--- a/src/solver/GurobiLpSolver.cpp
+++ b/src/solver/GurobiLpSolver.cpp
@@ -26,7 +26,7 @@ namespace storm {
// Create the environment.
int error = GRBloadenv(&env, "");
if (error || env == nullptr) {
- LOG4CPLUS_ERROR(logger, "Could not initialize Gurobi (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_ERROR("Could not initialize Gurobi (" << GRBgeterrormsg(env) << ", error code " << error << ").");
throw storm::exceptions::InvalidStateException() << "Could not initialize Gurobi environment (" << GRBgeterrormsg(env) << ", error code " << error << ").";
}
@@ -36,7 +36,7 @@ namespace storm {
// Create the model.
error = GRBnewmodel(env, &model, name.c_str(), 0, nullptr, nullptr, nullptr, nullptr, nullptr);
if (error) {
- LOG4CPLUS_ERROR(logger, "Could not initialize Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ").");
+ STORM_LOG_ERROR("Could not initialize Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ").");
throw storm::exceptions::InvalidStateException() << "Could not initialize Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ").";
}
}
@@ -346,7 +346,7 @@ namespace storm {
void GurobiLpSolver::writeModelToFile(std::string const& filename) const {
int error = GRBwrite(model, filename.c_str());
if (error) {
- LOG4CPLUS_ERROR(logger, "Unable to write Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ") to file.");
+ STORM_LOG_ERROR("Unable to write Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ") to file.");
throw storm::exceptions::InvalidStateException() << "Unable to write Gurobi model (" << GRBgeterrormsg(env) << ", error code " << error << ") to file.";
}
}
diff --git a/src/solver/NativeMinMaxLinearEquationSolver.cpp b/src/solver/NativeMinMaxLinearEquationSolver.cpp
index 22ccf956c..ec369ee3e 100644
--- a/src/solver/NativeMinMaxLinearEquationSolver.cpp
+++ b/src/solver/NativeMinMaxLinearEquationSolver.cpp
@@ -65,9 +65,9 @@ namespace storm {
// Check if the solver converged and issue a warning otherwise.
if (converged) {
- LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterations << " iterations.");
+ STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations.");
} else {
- LOG4CPLUS_WARN(logger, "Iterative solver did not converge after " << iterations << " iterations.");
+ STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations.");
}
// If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result
@@ -147,9 +147,9 @@ namespace storm {
// Check if the solver converged and issue a warning otherwise.
if (converged) {
- LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterations << " iterations.");
+ STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations.");
} else {
- LOG4CPLUS_WARN(logger, "Iterative solver did not converge after " << iterations << " iterations.");
+ STORM_LOG_WARN("Iterative solver did not converge after " << iterations << " iterations.");
}
// If requested, we store the scheduler for retrieval.
diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp
index f16c92a07..bb912371b 100644
--- a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp
+++ b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp
@@ -73,10 +73,10 @@ namespace storm {
// For testing only
if (sizeof(ValueType) == sizeof(double)) {
//std::cout << "<<< Using CUDA-DOUBLE Kernels >>>" << std::endl;
- LOG4CPLUS_INFO(logger, "<<< Using CUDA-DOUBLE Kernels >>>");
+ STORM_LOG_INFO("<<< Using CUDA-DOUBLE Kernels >>>");
} else {
//std::cout << "<<< Using CUDA-FLOAT Kernels >>>" << std::endl;
- LOG4CPLUS_INFO(logger, "<<< Using CUDA-FLOAT Kernels >>>");
+ STORM_LOG_INFO("<<< Using CUDA-FLOAT Kernels >>>");
}
// Now, we need to determine the SCCs of the MDP and perform a topological sort.
@@ -107,12 +107,12 @@ namespace storm {
} else {
result = __basicValueIteration_mvReduce_maximize<uint_fast64_t, ValueType>(this->maximalNumberOfIterations, this->precision, this->relative, A.rowIndications, A.columnsAndValues, x, b, nondeterministicChoiceIndices, globalIterations);
}
- LOG4CPLUS_INFO(logger, "Executed " << globalIterations << " of max. " << maximalNumberOfIterations << " Iterations on GPU.");
+ STORM_LOG_INFO("Executed " << globalIterations << " of max. " << maximalNumberOfIterations << " Iterations on GPU.");
bool converged = false;
if (!result) {
converged = false;
- LOG4CPLUS_ERROR(logger, "An error occurred in the CUDA Plugin. Can not continue.");
+ STORM_LOG_ERROR("An error occurred in the CUDA Plugin. Can not continue.");
throw storm::exceptions::InvalidStateException() << "An error occurred in the CUDA Plugin. Can not continue.";
} else {
converged = true;
@@ -120,12 +120,12 @@ namespace storm {
// Check if the solver converged and issue a warning otherwise.
if (converged) {
- LOG4CPLUS_INFO(logger, "Iterative solver converged after " << globalIterations << " iterations.");
+ STORM_LOG_INFO("Iterative solver converged after " << globalIterations << " iterations.");
} else {
- LOG4CPLUS_WARN(logger, "Iterative solver did not converged after " << globalIterations << " iterations.");
+ STORM_LOG_WARN("Iterative solver did not converged after " << globalIterations << " iterations.");
}
#else
- LOG4CPLUS_ERROR(logger, "The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!");
+ STORM_LOG_ERROR("The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!");
throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!";
#endif
} else {
@@ -139,7 +139,7 @@ namespace storm {
// Calculate the optimal distribution of sccs
std::vector<std::pair<bool, storm::storage::StateBlock>> optimalSccs = this->getOptimalGroupingFromTopologicalSccDecomposition(sccDecomposition, topologicalSort, this->A);
- LOG4CPLUS_INFO(logger, "Optimized SCC Decomposition, originally " << topologicalSort.size() << " SCCs, optimized to " << optimalSccs.size() << " SCCs.");
+ STORM_LOG_INFO("Optimized SCC Decomposition, originally " << topologicalSort.size() << " SCCs, optimized to " << optimalSccs.size() << " SCCs.");
std::vector<ValueType>* currentX = nullptr;
std::vector<ValueType>* swap = nullptr;
@@ -198,9 +198,9 @@ namespace storm {
#ifdef STORM_HAVE_CUDA
STORM_LOG_THROW(resetCudaDevice(), storm::exceptions::InvalidStateException, "Could not reset CUDA Device, can not use CUDA-based equation solver.");
- //LOG4CPLUS_INFO(logger, "Device has " << getTotalCudaMemory() << " Bytes of Memory with " << getFreeCudaMemory() << "Bytes free (" << (static_cast<double>(getFreeCudaMemory()) / static_cast<double>(getTotalCudaMemory())) * 100 << "%).");
- //LOG4CPLUS_INFO(logger, "We will allocate " << (sizeof(uint_fast64_t)* sccSubmatrix.rowIndications.size() + sizeof(uint_fast64_t)* sccSubmatrix.columnsAndValues.size() * 2 + sizeof(double)* sccSubX.size() + sizeof(double)* sccSubX.size() + sizeof(double)* sccSubB.size() + sizeof(double)* sccSubB.size() + sizeof(uint_fast64_t)* sccSubNondeterministicChoiceIndices.size()) << " Bytes.");
- //LOG4CPLUS_INFO(logger, "The CUDA Runtime Version is " << getRuntimeCudaVersion());
+ //STORM_LOG_INFO("Device has " << getTotalCudaMemory() << " Bytes of Memory with " << getFreeCudaMemory() << "Bytes free (" << (static_cast<double>(getFreeCudaMemory()) / static_cast<double>(getTotalCudaMemory())) * 100 << "%).");
+ //STORM_LOG_INFO("We will allocate " << (sizeof(uint_fast64_t)* sccSubmatrix.rowIndications.size() + sizeof(uint_fast64_t)* sccSubmatrix.columnsAndValues.size() * 2 + sizeof(double)* sccSubX.size() + sizeof(double)* sccSubX.size() + sizeof(double)* sccSubB.size() + sizeof(double)* sccSubB.size() + sizeof(uint_fast64_t)* sccSubNondeterministicChoiceIndices.size()) << " Bytes.");
+ //STORM_LOG_INFO("The CUDA Runtime Version is " << getRuntimeCudaVersion());
bool result = false;
localIterations = 0;
@@ -209,11 +209,11 @@ namespace storm {
} else {
result = __basicValueIteration_mvReduce_maximize<uint_fast64_t, ValueType>(this->maximalNumberOfIterations, this->precision, this->relative, sccSubmatrix.rowIndications, sccSubmatrix.columnsAndValues, *currentX, sccSubB, sccSubNondeterministicChoiceIndices, localIterations);
}
- LOG4CPLUS_INFO(logger, "Executed " << localIterations << " of max. " << maximalNumberOfIterations << " Iterations on GPU.");
+ STORM_LOG_INFO("Executed " << localIterations << " of max. " << maximalNumberOfIterations << " Iterations on GPU.");
if (!result) {
converged = false;
- LOG4CPLUS_ERROR(logger, "An error occurred in the CUDA Plugin. Can not continue.");
+ STORM_LOG_ERROR("An error occurred in the CUDA Plugin. Can not continue.");
throw storm::exceptions::InvalidStateException() << "An error occurred in the CUDA Plugin. Can not continue.";
} else {
converged = true;
@@ -226,12 +226,12 @@ namespace storm {
}
globalIterations += localIterations;
#else
- LOG4CPLUS_ERROR(logger, "The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!");
+ STORM_LOG_ERROR("The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!");
throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!";
#endif
} else {
//std::cout << "WARNING: Using CPU based TopoSolver! (double)" << std::endl;
- LOG4CPLUS_INFO(logger, "Performance Warning: Using CPU based TopoSolver! (double)");
+ STORM_LOG_INFO("Performance Warning: Using CPU based TopoSolver! (double)");
localIterations = 0;
converged = false;
while (!converged && localIterations < this->maximalNumberOfIterations) {
@@ -263,7 +263,7 @@ namespace storm {
++localIterations;
++globalIterations;
}
- LOG4CPLUS_INFO(logger, "Executed " << localIterations << " of max. " << this->maximalNumberOfIterations << " Iterations.");
+ STORM_LOG_INFO("Executed " << localIterations << " of max. " << this->maximalNumberOfIterations << " Iterations.");
}
@@ -289,9 +289,9 @@ namespace storm {
// Check if the solver converged and issue a warning otherwise.
if (converged) {
- LOG4CPLUS_INFO(logger, "Iterative solver converged after " << currentMaxLocalIterations << " iterations.");
+ STORM_LOG_INFO("Iterative solver converged after " << currentMaxLocalIterations << " iterations.");
} else {
- LOG4CPLUS_WARN(logger, "Iterative solver did not converged after " << currentMaxLocalIterations << " iterations.");
+ STORM_LOG_WARN("Iterative solver did not converged after " << currentMaxLocalIterations << " iterations.");
}
}
}
diff --git a/src/utility/ErrorHandling.h b/src/utility/ErrorHandling.h
index 5b9b50bdc..9bc228d6e 100644
--- a/src/utility/ErrorHandling.h
+++ b/src/utility/ErrorHandling.h
@@ -49,7 +49,7 @@ std::string demangle(char const* symbol) {
if (!SymInitialize(hProcess, NULL, TRUE)) {
// SymInitialize failed
error = GetLastError();
- LOG4CPLUS_ERROR(logger, "SymInitialize returned error : " << error);
+ STORM_LOG_ERROR("SymInitialize returned error : " << error);
return FALSE;
} else {
char demangled[1024];
@@ -58,7 +58,7 @@ std::string demangle(char const* symbol) {
} else {
// UnDecorateSymbolName failed
DWORD error = GetLastError();
- LOG4CPLUS_ERROR(logger, "UnDecorateSymbolName returned error: " << error);
+ STORM_LOG_ERROR("UnDecorateSymbolName returned error: " << error);
}
}
#endif
@@ -87,7 +87,7 @@ void printUsage();
* @param sig The code of the signal that needs to be handled.
*/
void signalHandler(int sig) {
- LOG4CPLUS_FATAL(logger, "The program received signal " << sig << ". The following backtrace shows the status upon reception of the signal.");
+ STORM_LOG_ERROR("The program received signal " << sig << ". The following backtrace shows the status upon reception of the signal.");
printUsage();
#ifndef WINDOWS
# define SIZE 128
@@ -106,13 +106,13 @@ void signalHandler(int sig) {
// Starting this for-loop at j=2 means that we skip the handler itself. Currently this is not
// done.
for (int j = 1; j < nptrs; j++) {
- LOG4CPLUS_FATAL(logger, nptrs-j << ": " << demangle(strings[j]));
+ STORM_LOG_ERROR(nptrs-j << ": " << demangle(strings[j]));
}
free(strings);
#else
- LOG4CPLUS_WARN(logger, "No Backtrace Support available on Platform Windows!");
+ STORM_LOG_WARN("No Backtrace Support available on Platform Windows!");
#endif
- LOG4CPLUS_FATAL(logger, "Exiting.");
+ STORM_LOG_ERROR("Exiting.");
exit(2);
}
diff --git a/src/utility/cstring.cpp b/src/utility/cstring.cpp
index 71bcbe69a..d80059e94 100644
--- a/src/utility/cstring.cpp
+++ b/src/utility/cstring.cpp
@@ -25,8 +25,8 @@ namespace cstring {
uint_fast64_t checked_strtol(char const* str, char const** end) {
uint_fast64_t res = strtol(str, const_cast<char**>(end), 10);
if (str == *end) {
- LOG4CPLUS_ERROR(logger, "Error while parsing integer. Next input token is not a number.");
- LOG4CPLUS_ERROR(logger, "\tUpcoming input is: \"" << std::string(str, 0, 16) << "\"");
+ STORM_LOG_ERROR("Error while parsing integer. Next input token is not a number.");
+ STORM_LOG_ERROR("\tUpcoming input is: \"" << std::string(str, 0, 16) << "\"");
throw storm::exceptions::WrongFormatException("Error while parsing integer. Next input token is not a number.");
}
return res;
@@ -43,8 +43,8 @@ uint_fast64_t checked_strtol(char const* str, char const** end) {
double checked_strtod(char const* str, char const** end) {
double res = strtod(str, const_cast<char**>(end));
if (str == *end) {
- LOG4CPLUS_ERROR(logger, "Error while parsing floating point. Next input token is not a number.");
- LOG4CPLUS_ERROR(logger, "\tUpcoming input is: \"" << std::string(str, 0, 16) << "\"");
+ STORM_LOG_ERROR("Error while parsing floating point. Next input token is not a number.");
+ STORM_LOG_ERROR("\tUpcoming input is: \"" << std::string(str, 0, 16) << "\"");
throw storm::exceptions::WrongFormatException("Error while parsing floating point. Next input token is not a number.");
}
return res;
diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp
index 0aa8b2836..e4839b1aa 100644
--- a/src/utility/graph.cpp
+++ b/src/utility/graph.cpp
@@ -829,7 +829,7 @@ namespace storm {
template <typename T>
std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<T> const& matrix) {
if (matrix.getRowCount() != matrix.getColumnCount()) {
- LOG4CPLUS_ERROR(logger, "Provided matrix is required to be square.");
+ STORM_LOG_ERROR("Provided matrix is required to be square.");
throw storm::exceptions::InvalidArgumentException() << "Provided matrix is required to be square.";
}
@@ -903,7 +903,7 @@ namespace storm {
storm::storage::BitVector const& startingStates,
storm::storage::BitVector const* filterStates) {
- LOG4CPLUS_INFO(logger, "Performing Dijkstra search.");
+ STORM_LOG_INFO("Performing Dijkstra search.");
const uint_fast64_t noPredecessorValue = storm::utility::zero<uint_fast64_t>();
std::vector<T> probabilities(model.getNumberOfStates(), storm::utility::zero<T>());
@@ -949,7 +949,7 @@ namespace storm {
std::pair<std::vector<T>, std::vector<uint_fast64_t>> result;
result.first = std::move(probabilities);
result.second = std::move(predecessors);
- LOG4CPLUS_INFO(logger, "Done performing Dijkstra search.");
+ STORM_LOG_INFO("Done performing Dijkstra search.");
return result;
}
diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
index b293e2a4f..b2a39f5dd 100644
--- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
+++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
@@ -78,7 +78,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
EXPECT_NEAR(0.9993949793, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
- auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
+ auto reachabilityRewardFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula, storm::logic::FormulaContext::Reward);
result = checker.check(*reachabilityRewardFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
diff --git a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
index eda9620df..23949131a 100644
--- a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
+++ b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
@@ -79,7 +79,7 @@ TEST(NativeDtmcPrctlModelCheckerTest, SynchronousLeader) {
EXPECT_NEAR(0.9993949793, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
- auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
+ auto reachabilityRewardFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula, storm::logic::FormulaContext::Reward);
result = checker.check(*reachabilityRewardFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();