diff --git a/examples/mdp/csma/csma3_4.nm b/examples/mdp/csma/csma3_4.nm index c1b97fc3f..8739053e5 100644 --- a/examples/mdp/csma/csma3_4.nm +++ b/examples/mdp/csma/csma3_4.nm @@ -129,4 +129,6 @@ endrewards label "all_delivered" = s1=4&s2=4&s3=4; label "one_delivered" = s1=4|s2=4|s3=4; label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2); - +formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1,s3=4?cd3:K+1); +formula min_collisions = min(cd1,cd2,cd3); +formula max_collisions = max(cd1,cd2,cd3); diff --git a/examples/mdp/csma/csma4_4.nm b/examples/mdp/csma/csma4_4.nm index 90f182dde..e1ba511f4 100644 --- a/examples/mdp/csma/csma4_4.nm +++ b/examples/mdp/csma/csma4_4.nm @@ -134,4 +134,6 @@ endrewards label "all_delivered" = s1=4&s2=4&s3=4&s4=4; label "one_delivered" = s1=4|s2=4|s3=4|s4=4; label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2)|(cd4=K & s4=1 & b=2); - +formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1,s3=4?cd3:K+1,s4=4?cd4:K+1); +formula min_collisions = min(cd1,cd2,cd3,cd4); +formula max_collisions = max(cd1,cd2,cd3,cd4); diff --git a/examples/mdp/csma/csma4_6.nm b/examples/mdp/csma/csma4_6.nm index 8e9fb110a..12e5f0152 100644 --- a/examples/mdp/csma/csma4_6.nm +++ b/examples/mdp/csma/csma4_6.nm @@ -136,4 +136,6 @@ endrewards label "all_delivered" = s1=4&s2=4&s3=4&s4=4; label "one_delivered" = s1=4|s2=4|s3=4|s4=4; label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2)|(cd4=K & s4=1 & b=2); - +formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1,s3=4?cd3:K+1,s4=4?cd4:K+1); +formula min_collisions = min(cd1,cd2,cd3,cd4); +formula max_collisions = max(cd1,cd2,cd3,cd4); diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp index f6ff87f5b..7054e26ef 100644 --- a/src/parser/ExpressionParser.cpp +++ b/src/parser/ExpressionParser.cpp @@ -337,12 +337,8 @@ namespace storm { STORM_LOG_THROW(this->identifiers_ != nullptr, storm::exceptions::WrongFormatException, "Unable to substitute identifier expressions without given mapping."); storm::expressions::Expression const* expression = this->identifiers_->find(identifier); if (expression == nullptr) { - if (allowBacktracking) { - pass = false; - return manager->boolean(false); - } else { - pass = false; - } + pass = false; + return manager->boolean(false); } return *expression; } else { diff --git a/src/parser/SpiritErrorHandler.h b/src/parser/SpiritErrorHandler.h index 3e78935bd..cd2a35b06 100644 --- a/src/parser/SpiritErrorHandler.h +++ b/src/parser/SpiritErrorHandler.h @@ -22,7 +22,7 @@ namespace storm { stream << "Parsing error at " << get_line(where) << ":" << boost::spirit::get_column(lineStart, where) << ": " << " expecting " << what << ", here:" << std::endl; stream << "\t" << line << std::endl << "\t"; auto caretColumn = boost::spirit::get_column(lineStart, where); - stream << std::string(caretColumn - 1, ' ') << "^" << std::endl; + stream << "\t" << std::string(caretColumn - 1, ' ') << "^" << std::endl; STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, stream.str()); return qi::fail;