Made counterexample generation output usable.

-std::cout gives enough information to understand what th result of the generaton is.
-Added another argument to --counterExample specifying a directory to write .dot files containing the critical subsystems (as Dtmc) to.
-Cleaned up some logging output of the counterexample generationn.

Next up: Merging.


Former-commit-id: feb4323052

src/counterexamples/PathBasedSubsystemGenerator.h

@@ -617,8 +617,11 @@ public:
 		if((initStates & targetStates).getNumberOfSetBits() != 0) {
 			subSys.set((initStates & targetStates).getSetIndicesList().front(), true);
 
-			LOG4CPLUS_INFO(logger, "Critical subsystem: " << subSys.toString());
-			std::cout << "Critical subsystem: " << subSys.toString() << std::endl;
+			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);
 
 			return model.getSubDtmc(subSys);
 		}
@@ -692,17 +695,11 @@ public:
 			}
 		}
 
-#ifdef BENCHMARK
 		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);
-		//LOG4CPLUS_INFO(logger, "Critical subsystem: " << subSys.toString());
-#else
-		LOG4CPLUS_INFO(logger, "Critical subsystem: " << subSys.toString());
-		std::cout << "Critical subsystem: " << subSys.toString() << std::endl;
-#endif
 
 		return model.getSubDtmc(subSys);
 	}

src/storm.cpp

@@ -262,6 +262,23 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double>
  * Handles the counterexample generation control.
  */
  void generateCounterExample(storm::parser::AutoParser<double> parser) {
+	LOG4CPLUS_INFO(logger, "Starting counterexample generation.");
+	LOG4CPLUS_INFO(logger, "Testing inputs...");
+
+	//First test output directory.
+	std::string outPath = storm::settings::Settings::getInstance()->getOptionByLongName("counterExample").getArgument(1).getValueAsString();
+	if(outPath.back() != '/' && outPath.back() != '\\') {
+		LOG4CPLUS_ERROR(logger, "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.");
+		return;
+	}
+	testFile.close();
+	std::remove((outPath + "test.dot").c_str());
+
  	//Differentiate between model types.
 	if(parser.getType() != storm::models::DTMC) {
 		LOG4CPLUS_ERROR(logger, "Counterexample generation for the selected model type is not supported.");
@@ -282,6 +299,25 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double>
 		return;
 	}
 
+	// Get prctl file name without the filetype
+	uint_fast64_t first = 0;
+	if(chosenPrctlFile.find('/') != std::string::npos) {
+		first = chosenPrctlFile.find_last_of('/') + 1;
+	} else if(chosenPrctlFile.find('\\') != std::string::npos) {
+		first = chosenPrctlFile.find_last_of('\\') + 1;
+	}
+
+	uint_fast64_t length;
+	if(chosenPrctlFile.find_last_of('.') != std::string::npos && chosenPrctlFile.find_last_of('.') >= first) {
+		length = chosenPrctlFile.find_last_of('.') - first;
+	} else {
+		length = chosenPrctlFile.length() - first;
+	}
+
+	std::string outFileName = chosenPrctlFile.substr(first, length);
+
+	// Test formulas and do generation
+	uint_fast64_t fIndex = 0;
 	for (auto formula : formulaList) {
 
 		// First check if it is a formula type for which a counterexample can be generated.
@@ -293,21 +329,41 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double>
 
 		storm::property::prctl::AbstractStateFormula<double> const& stateForm = static_cast<storm::property::prctl::AbstractStateFormula<double> const&>(*formula);
 
+		// Do some output
+		std::cout << "Generating counterexample for formula " << fIndex << ":" << std::endl;
+		LOG4CPLUS_INFO(logger, "Generating counterexample for formula " + std::to_string(fIndex) + ": ");
+		std::cout << "\t" << formula->toString() << "\n" << std::endl;
+		LOG4CPLUS_INFO(logger, 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.
 		storm::storage::BitVector result = stateForm.check(*createPrctlModelChecker(model));
 		if((result & model.getInitialStates()).getNumberOfSetBits() == model.getInitialStates().getNumberOfSetBits()) {
-			LOG4CPLUS_ERROR(logger, "Formula is satisfied. Can not generate counterexample.");
+			std::cout << "Formula is satisfied. Can not generate counterexample.\n\n" << std::endl;
+			LOG4CPLUS_INFO(logger, "Formula is satisfied. Can not generate counterexample.");
 			delete formula;
 			continue;
 		}
 
-		//Generate counterexample
+		// Generate counterexample
 		storm::models::Dtmc<double> counterExample = storm::counterexamples::PathBasedSubsystemGenerator<double>::computeCriticalSubsystem(*parser.getModel<storm::models::Dtmc<double>>(), stateForm);
 
-		//Output counterexample
+		LOG4CPLUS_INFO(logger, "Found counterexample.");
+
+		// Output counterexample
+		// Do standard output
+		std::cout << "Found counterexample with following properties: " << std::endl;
 		counterExample.printModelInformationToStream(std::cout);
+		std::cout << "For full Dtmc see " << outFileName << "_" << fIndex << ".dot at given output path.\n\n" << std::endl;
+
+		// Write the .dot file
+		std::ofstream outFile(outPath + outFileName + "_" + std::to_string(fIndex) + ".dot");
+		if(outFile.good()) {
+			counterExample.writeDotToStream(outFile, true, nullptr, nullptr, nullptr, nullptr, nullptr, nullptr, true);
+			outFile.close();
+		}
 
+		fIndex++;
 		delete formula;
 	}
  }

src/utility/StormOptions.cpp

@@ -12,7 +12,7 @@ bool storm::utility::StormOptions::optionsRegistered = storm::settings::Settings
 	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "prctl", "", "Evaluates the PRCTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read PRCTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
 	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "csl", "", "Evaluates the CSL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("cslFileName", "The path and name of the File to read CSL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
 	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "ltl", "", "Evaluates the LTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("ltlFileName", "The path and name of the File to read LTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
-	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "counterExample", "", "Generates a counterexample for the given formulas if not satisfied by the model").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read the PRCTL Formulas to be used in \n\t\t\t\t\t\t the couterexample generation from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "counterExample", "", "Generates a counterexample for the given formulas if not satisfied by the model").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read the PRCTL Formulas to be used in \n\t\t\t\t\t\t the couterexample generation from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).addArgument(storm::settings::ArgumentBuilder::createStringArgument("outputPath", "The path to the directory to write the generated counterexample files to.").build()).build());
 	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "transitionRewards", "", "If specified, the model will have these transition rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionRewardsFileName", "The path and name of the File to read the Transition Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
 	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "stateRewards", "", "If specified, the model will have these state rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("stateRewardsFileName", "The path and name of the File to read the State Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
 	settings->addOption(storm::settings::OptionBuilder("StoRM Main", "fixDeadlocks", "", "Insert Self-Loops for States with no outgoing transitions").build());