sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
3600 Commits
2 Branches
0 Tags
187 MiB
 
 
 
 
Tree: 5a793839e9
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '5a793839e9'
${ noResults }
tempest/src/storage/expressions/ToCppVisitor.cpp

289 lines
13 KiB
Raw Blame History

#include "src/storage/expressions/ToCppVisitor.h"
#include "src/storage/expressions/Expressions.h"
namespace storm {
namespace expressions {
ToCppTranslationOptions::ToCppTranslationOptions(std::unordered_map<storm::expressions::Variable, std::string> const& prefixes, std::unordered_map<storm::expressions::Variable, std::string> const& names, std::string const& valueTypeCast) : prefixes(prefixes), names(names), valueTypeCast(valueTypeCast) {
// Intentionally left empty.
}
std::unordered_map<storm::expressions::Variable, std::string> const& ToCppTranslationOptions::getPrefixes() const {
return prefixes;
}
std::unordered_map<storm::expressions::Variable, std::string> const& ToCppTranslationOptions::getNames() const {
return names;
}
bool ToCppTranslationOptions::hasValueTypeCast() const {
return !valueTypeCast.empty();
}
std::string const& ToCppTranslationOptions::getValueTypeCast() const {
return valueTypeCast;
}
void ToCppTranslationOptions::clearValueTypeCast() {
valueTypeCast = "";
}
std::string ToCppVisitor::translate(storm::expressions::Expression const& expression, ToCppTranslationOptions const& options) {
expression.accept(*this, options);
std::string result = stream.str();
stream.str("");
return result;
}
boost::any ToCppVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) {
ToCppTranslationOptions conditionOptions = boost::any_cast<ToCppTranslationOptions>(data);
conditionOptions.clearValueTypeCast();
stream << "(";
expression.getCondition()->accept(*this, conditionOptions);
stream << " ? ";
expression.getThenExpression()->accept(*this, data);
stream << " : ";
expression.getElseExpression()->accept(*this, data);
stream << ")";
return boost::none;
}
boost::any ToCppVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
ToCppTranslationOptions newOptions = boost::any_cast<ToCppTranslationOptions>(data);
newOptions.clearValueTypeCast();
switch (expression.getOperatorType()) {
case BinaryBooleanFunctionExpression::OperatorType::And:
stream << "(";
expression.getFirstOperand()->accept(*this, newOptions);
stream << " && ";
expression.getSecondOperand()->accept(*this, newOptions);
stream << ")";
break;
case BinaryBooleanFunctionExpression::OperatorType::Or:
stream << "(";
expression.getFirstOperand()->accept(*this, newOptions);
stream << " || ";
expression.getSecondOperand()->accept(*this, newOptions);
stream << ")";
break;
case BinaryBooleanFunctionExpression::OperatorType::Xor:
stream << "(";
expression.getFirstOperand()->accept(*this, newOptions);
stream << " ^ ";
expression.getSecondOperand()->accept(*this, newOptions);
stream << ")";
break;
case BinaryBooleanFunctionExpression::OperatorType::Implies:
stream << "(!";
expression.getFirstOperand()->accept(*this, newOptions);
stream << " || ";
expression.getSecondOperand()->accept(*this, newOptions);
stream << ")";
break;
case BinaryBooleanFunctionExpression::OperatorType::Iff:
stream << "!(";
expression.getFirstOperand()->accept(*this, newOptions);
stream << " ^ ";
expression.getSecondOperand()->accept(*this, newOptions);
stream << ")";
break;
}
return boost::none;
}
boost::any ToCppVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
switch (expression.getOperatorType()) {
case BinaryNumericalFunctionExpression::OperatorType::Plus:
stream << "(";
expression.getFirstOperand()->accept(*this, data);
stream << " + ";
expression.getSecondOperand()->accept(*this, data);
stream << ")";
break;
case BinaryNumericalFunctionExpression::OperatorType::Minus:
stream << "(";
expression.getFirstOperand()->accept(*this, data);
stream << " - ";
expression.getSecondOperand()->accept(*this, data);
stream << ")";
break;
case BinaryNumericalFunctionExpression::OperatorType::Times:
stream << "(";
expression.getFirstOperand()->accept(*this, data);
stream << " * ";
expression.getSecondOperand()->accept(*this, data);
stream << ")";
break;
case BinaryNumericalFunctionExpression::OperatorType::Divide:
stream << "(";
expression.getFirstOperand()->accept(*this, data);
stream << " / ";
expression.getSecondOperand()->accept(*this, data);
stream << ")";
break;
case BinaryNumericalFunctionExpression::OperatorType::Min:
stream << "std::min(";
expression.getFirstOperand()->accept(*this, data);
stream << ", ";
expression.getSecondOperand()->accept(*this, data);
stream << ")";
break;
case BinaryNumericalFunctionExpression::OperatorType::Max:
stream << "std::max(";
expression.getFirstOperand()->accept(*this, data);
stream << ", ";
expression.getSecondOperand()->accept(*this, data);
stream << ")";
break;
case BinaryNumericalFunctionExpression::OperatorType::Power:
stream << "std::pow(";
expression.getFirstOperand()->accept(*this, data);
stream << ", ";
expression.getSecondOperand()->accept(*this, data);
stream << ")";
break;
}
return boost::none;
}
boost::any ToCppVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) {
ToCppTranslationOptions newOptions = boost::any_cast<ToCppTranslationOptions>(data);
newOptions.clearValueTypeCast();
switch (expression.getRelationType()) {
case BinaryRelationExpression::RelationType::Equal:
stream << "(";
expression.getFirstOperand()->accept(*this, newOptions);
stream << " == ";
expression.getSecondOperand()->accept(*this, newOptions);
stream << ")";
break;
case BinaryRelationExpression::RelationType::NotEqual:
stream << "(";
expression.getFirstOperand()->accept(*this, newOptions);
stream << " != ";
expression.getSecondOperand()->accept(*this, newOptions);
stream << ")";
break;
case BinaryRelationExpression::RelationType::Less:
stream << "(";
expression.getFirstOperand()->accept(*this, newOptions);
stream << " < ";
expression.getSecondOperand()->accept(*this, newOptions);
stream << ")";
break;
case BinaryRelationExpression::RelationType::LessOrEqual:
stream << "(";
expression.getFirstOperand()->accept(*this, newOptions);
stream << " <= ";
expression.getSecondOperand()->accept(*this, newOptions);
stream << ")";
break;
case BinaryRelationExpression::RelationType::Greater:
stream << "(";
expression.getFirstOperand()->accept(*this, newOptions);
stream << " > ";
expression.getSecondOperand()->accept(*this, newOptions);
stream << ")";
break;
case BinaryRelationExpression::RelationType::GreaterOrEqual:
stream << "(";
expression.getFirstOperand()->accept(*this, newOptions);
stream << " >= ";
expression.getSecondOperand()->accept(*this, newOptions);
stream << ")";
break;
}
return boost::none;
}
boost::any ToCppVisitor::visit(VariableExpression const& expression, boost::any const& data) {
ToCppTranslationOptions const& options = boost::any_cast<ToCppTranslationOptions const&>(data);
if (options.hasValueTypeCast()) {
stream << "static_cast<" << options.getValueTypeCast() << ">(";
}
auto prefixIt = options.getPrefixes().find(expression.getVariable());
if (prefixIt != options.getPrefixes().end()) {
auto nameIt = options.getNames().find(expression.getVariable());
if (nameIt != options.getNames().end()) {
stream << prefixIt->second << nameIt->second;
} else {
stream << prefixIt->second << expression.getVariableName();
}
} else {
auto nameIt = options.getNames().find(expression.getVariable());
if (nameIt != options.getNames().end() (newInstance'=true) & (runCount'=TotalRuns) & (launch'=false); // Set up a newInstance protocol instance [] newInstance & runCount>0 -> (runCount'=runCount-1) & (newInstance'=false) & (start'=true); // SENDER // Start the protocol [] start -> (lastSeen'=0) & (run'=true) & (deliver'=false) & (start'=false); // CROWD MEMBERS // Good or bad crowd member? [] !good & !bad & !deliver & run -> 1-badC : (good'=true) & (recordLast'=true) & (run'=false) + badC : (bad'=true) & (badObserve'=true) & (run'=false); // GOOD MEMBERS // Forward with probability PF, else deliver [] good & !deliver & run -> PF : (good'=false) + 1-PF : (deliver'=true); // Record the last crowd member who touched the msg; // all good members may appear with equal probability // Note: This is backward. In the real protocol, each honest // forwarder randomly chooses the next forwarder. // Here, the identity of an honest forwarder is randomly // chosen *after* it has forwarded the message. [] recordLast & CrowdSize=2 -> 1/2 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + 1/2 : (lastSeen'=1) & (recordLast'=false) & (run'=true); [] recordLast & CrowdSize=3 -> 1/3 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + 1/3 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + 1/3 : (lastSeen'=2) & (recordLast'=false) & (run'=true); [] recordLast & CrowdSize=4 -> 1/4 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + 1/4 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + 1/4 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + 1/4 : (lastSeen'=3) & (recordLast'=false) & (run'=true); [] recordLast & CrowdSize=5 -> 1/5 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + 1/5 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + 1/5 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + 1/5 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + 1/5 : (lastSeen'=4) & (recordLast'=false) & (run'=true); [] recordLast & CrowdSize=10 -> 1/10 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + 1/10 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + 1/10 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + 1/10 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + 1/10 : (lastSeen'=4) & (recordLast'=false) & (run'=true) + 1/10 : (lastSeen'=5) & (recordLast'=false) & (run'=true) + 1/10 : (lastSeen'=6) & (recordLast'=false) & (run'=true) + 1/10 : (lastSeen'=7) & (recordLast'=false) & (run'=true) + 1/10 : (lastSeen'=8) & (recordLast'=false) & (run'=true) + 1/10 : (lastSeen'=9) & (recordLast'=false) & (run'=true); [] recordLast & CrowdSize=15 -> 1/15 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + 1/15 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + 1/15 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + 1/15 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + 1/15 : (lastSeen'=4) & (recordLast'=false) & (run'=true) + 1/15 : (lastSeen'=5) & (recordLast'=false) & (run'=true) + 1/15 : (lastSeen'=6) & (recordLast'=false) & (run'=true) + 1/15 : (lastSeen'=7) & (recordLast'=false) & (run'=true) + 1/15 : (lastSeen'=8) & (recordLast'=false) & (run'=true) + 1/15 : (lastSeen'=9) & (recordLast'=false) & (run'=true) + 1/15 : (lastSeen'=10) & (recordLast'=false) & (run'=true) + 1/15 : (lastSeen'=11) & (recordLast'=false) & (run'=true) + 1/15 : (lastSeen'=12) & (recordLast'=false) & (run'=true) + 1/15 : (lastSeen'=13) & (recordLast'=false) & (run'=true) + 1/15 : (lastSeen'=14) & (recordLast'=false) & (run'=true); [] recordLast & CrowdSize=20 -> 1/20 : (lastSeen'=0) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=1) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=2) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=3) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=4) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=5) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=6) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=7) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=8) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=9) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=10) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=11) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=12) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=13) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=14) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=15) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=16) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=17) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=18) & (recordLast'=false) & (run'=true) + 1/20 : (lastSeen'=19) & (recordLast'=false) & (run'=true); // BAD MEMBERS // Remember from whom the message was received and deliver // CWDMAX: 1 rule per each good crowd member [] lastSeen=0 & badObserve & observe0 (observe0' =observe0 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=1 & badObserve & observe1 (observe1' =observe1 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=2 & badObserve & observe2 (observe2' =observe2 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=3 & badObserve & observe3 (observe3' =observe3 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=4 & badObserve & observe4 (observe4' =observe4 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=5 & badObserve & observe5 (observe5' =observe5 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=6 & badObserve & observe6 (observe6' =observe6 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=7 & badObserve & observe7 (observe7' =observe7 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=8 & badObserve & observe8 (observe8' =observe8 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=9 & badObserve & observe9 (observe9' =observe9 +1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=10 & badObserve & observe10 (observe10'=observe10+1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=11 & badObserve & observe11 (observe11'=observe11+1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=12 & badObserve & observe12 (observe12'=observe12+1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=13 & badObserve & observe13 (observe13'=observe13+1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=14 & badObserve & observe14 (observe14'=observe14+1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=15 & badObserve & observe15 (observe15'=observe15+1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=16 & badObserve & observe16 (observe16'=observe16+1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=17 & badObserve & observe17 (observe17'=observe17+1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=18 & badObserve & observe18 (observe18'=observe18+1) & (deliver'=true) & (run'=true) & (badObserve'=false); [] lastSeen=19 & badObserve & observe19 (observe19'=observe19+1) & (deliver'=true) & (run'=true) & (badObserve'=false); // RECIPIENT // Delivery to destination [] deliver & run -> (done'=true) & (deliver'=false) & (run'=false) & (good'=false) & (bad'=false); // Start a newInstance instance [] done -> (newInstance'=true) & (done'=false) & (run'=false) & (lastSeen'=MaxGood); endmodule label "observe0Greater1" = observe0 > 1; label "observeIGreater1" = observe1>1|observe2>1; label "observeOnlyTrueSender" = observe0>1&observe1<=1 & observe2<=1;