Browse Source

Some code style and documentation

main
Lanchid 12 years ago
parent
commit
9bc8bb2ca8
  1. 7
      src/parser/PrctlFileParser.cpp
  2. 6
      src/parser/PrctlParser.h

7
src/parser/PrctlFileParser.cpp

@ -17,7 +17,7 @@ namespace storm {
namespace parser { namespace parser {
PrctlFileParser::PrctlFileParser(std::string filename, storm::models::Dtmc<double>& dtmc, enum libraries library) { PrctlFileParser::PrctlFileParser(std::string filename, storm::models::Dtmc<double>& dtmc, enum libraries library) {
//Here ,the model checker which uses the correct library is created and a reference stored in the pointer modelChecker:
storm::modelchecker::SparseDtmcPrctlModelChecker<double>* modelChecker = nullptr; storm::modelchecker::SparseDtmcPrctlModelChecker<double>* modelChecker = nullptr;
switch(library) { switch(library) {
//case EIGEN: //case EIGEN:
@ -30,11 +30,14 @@ PrctlFileParser::PrctlFileParser(std::string filename, storm::models::Dtmc<doubl
modelChecker = new storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>(dtmc); modelChecker = new storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
break; break;
} }
//Now, the check function (which works on abstract model checkers) can parse the formulas and invoke the model checker:
check(filename, modelChecker); check(filename, modelChecker);
delete modelChecker; delete modelChecker;
} }
PrctlFileParser::PrctlFileParser(std::string filename, storm::models::Mdp<double>& mdp, enum libraries library) { PrctlFileParser::PrctlFileParser(std::string filename, storm::models::Mdp<double>& mdp, enum libraries library) {
//Here ,the model checker which uses the correct library is created and a reference stored in the pointer modelChecker:
storm::modelchecker::SparseMdpPrctlModelChecker<double>* modelChecker = nullptr; storm::modelchecker::SparseMdpPrctlModelChecker<double>* modelChecker = nullptr;
switch(library) { switch(library) {
//case EIGEN: //case EIGEN:
@ -46,6 +49,8 @@ PrctlFileParser::PrctlFileParser(std::string filename, storm::models::Mdp<double
modelChecker = new storm::modelchecker::GmmxxMdpPrctlModelChecker<double>(mdp); modelChecker = new storm::modelchecker::GmmxxMdpPrctlModelChecker<double>(mdp);
break; break;
} }
//Now, the check function (which works on abstract model checkers) can parse the formulas and invoke the model checker:
check(filename, modelChecker); check(filename, modelChecker);
delete modelChecker; delete modelChecker;
} }

6
src/parser/PrctlParser.h

@ -18,8 +18,7 @@ namespace parser {
* This class creates a PctlFormula object which can be accessed through the getFormula() method (of base * This class creates a PctlFormula object which can be accessed through the getFormula() method (of base
* class PrctlParser). However, it will not delete this object. * class PrctlParser). However, it will not delete this object.
*/ */
class PrctlParser : Parser
{
class PrctlParser : Parser {
public: public:
/*! /*!
* Reads a PRCTL formula from its string representation and parses it into a formula tree, consisting of * Reads a PRCTL formula from its string representation and parses it into a formula tree, consisting of
@ -35,8 +34,7 @@ class PrctlParser : Parser
/*! /*!
* @return a pointer to the parsed formula object * @return a pointer to the parsed formula object
*/ */
storm::formula::AbstractFormula<double>* getFormula()
{
storm::formula::AbstractFormula<double>* getFormula() {
return this->formula; return this->formula;
} }

Loading…
Cancel
Save