diff --git a/CMakeLists.txt b/CMakeLists.txt index 40c0cbf5..63f00e0f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -19,6 +19,8 @@ set(CMAKE_PREFIX_PATH "${CMAKE_PREFIX_PATH};${CMAKE_CURRENT_SOURCE_DIR}/libs") add_compile_definitions(MODELS_DIR="${CMAKE_CURRENT_SOURCE_DIR}/test/models") +add_definitions(-DENABLE_CORA) + find_package(FLEX 2.6.4 REQUIRED) find_package(BISON 3.6.0 REQUIRED) if (${CMAKE_SYSTEM_NAME} STREQUAL Darwin) diff --git a/getlibs/getlibs.sh b/getlibs/getlibs.sh index dab3fd60..bde04656 100755 --- a/getlibs/getlibs.sh +++ b/getlibs/getlibs.sh @@ -14,6 +14,7 @@ fi for target in "$@" ; do LIBS="$LOCAL/$target" # libxml2 + echo $LIBS if [ ! -r "$LIBS/lib/libxml2.a" ] ; then echo -e "${BW}Preparing source of ${LIBXML2}${NC}" prepare_libxml2 diff --git a/include/utap/common.h b/include/utap/common.h index 08ea90d6..d380e89d 100644 --- a/include/utap/common.h +++ b/include/utap/common.h @@ -236,6 +236,7 @@ namespace UTAP LOCATION_EXPR, CHANNEL, COST, + REWARD, INVARIANT, INVARIANT_WR, GUARD, diff --git a/include/utap/document.h b/include/utap/document.h index 8ce24601..8bf90267 100644 --- a/include/utap/document.h +++ b/include/utap/document.h @@ -69,6 +69,7 @@ namespace UTAP expression_t invariant; /**< The invariant */ expression_t exponentialRate; expression_t costRate; /**< Rate expression */ + expression_t rewardRate; /**< Rate expression */ int32_t nr; /**< Location number in a template */ std::string str() const; }; diff --git a/include/utap/type.h b/include/utap/type.h index c820e16d..5098d25e 100644 --- a/include/utap/type.h +++ b/include/utap/type.h @@ -242,6 +242,9 @@ namespace UTAP /** Shortcut for is(COST). */ bool isCost() const { return is(Constants::COST); } + /** Shortcut for is(REWARD). */ + bool isReward() const { return is(Constants::REWARD); } + /** Shortcut for is(DOUBLE). */ bool isDouble() const { return is(Constants::DOUBLE); } diff --git a/src/document.cpp b/src/document.cpp index 0c49c302..e192070d 100644 --- a/src/document.cpp +++ b/src/document.cpp @@ -730,7 +730,8 @@ Document::Document() { global.frame = frame_t::create(); #ifdef ENABLE_CORA - addVariable(&global, type_t::createPrimitive(COST), "cost", expression_t()); + addVariable(&global, type_t::createPrimitive(REWARD), "reward", expression_t(), position_t()); + addVariable(&global, type_t::createPrimitive(COST), "cost", expression_t(), position_t()); #endif } diff --git a/src/type.cpp b/src/type.cpp index 7e3fa92f..7fccde8a 100644 --- a/src/type.cpp +++ b/src/type.cpp @@ -114,6 +114,7 @@ bool type_t::isPrefix() const case Constants::BRANCHPOINT: case Constants::CHANNEL: case Constants::COST: + case Constants::REWARD: case Constants::INVARIANT: case Constants::INVARIANT_WR: case Constants::GUARD: @@ -515,6 +516,8 @@ string type_t::str() const case Constants::COST: kind = "cost"; break; + case Constants::REWARD: kind = "reward"; break; + case Constants::RATE: kind = "rate"; break; case Constants::TYPEDEF: kind = "def"; break; @@ -627,6 +630,8 @@ string type_t::toDeclarationString() const case Constants::COST: kind = "cost"; break; + case Constants::REWARD: kind = "reward"; break; + case Constants::RATE: kind = "rate"; break; case Constants::TYPEDEF: diff --git a/src/typechecker.cpp b/src/typechecker.cpp index 234a51af..e75751e1 100644 --- a/src/typechecker.cpp +++ b/src/typechecker.cpp @@ -35,6 +35,8 @@ using namespace Constants; */ static bool isCost(expression_t expr) { return expr.getType().is(COST); } +static bool isReward(expression_t expr) {return expr.getType().is(REWARD); } + static bool isVoid(expression_t expr) { return expr.getType().isVoid(); } static bool isDouble(expression_t expr) { return expr.getType().isDouble(); } @@ -165,6 +167,7 @@ static bool isAssignable(type_t type) case Constants::STRING: case Constants::CLOCK: case Constants::COST: + case Constants::REWARD: case Constants::SCALAR: return true; case ARRAY: return isAssignable(type[0]); @@ -215,9 +218,11 @@ class RateDecomposer public: RateDecomposer() {} expression_t costRate; + expression_t rewardRate; expression_t invariant{expression_t::createConstant(1)}; bool hasStrictInvariant{false}, hasClockRates{false}; size_t countCostRates{0}; + size_t countRewardRates{0}; void decompose(expression_t, bool inforall = false); }; @@ -254,7 +259,10 @@ void RateDecomposer::decompose(expression_t expr, bool inforall) if (isCost(left)) { costRate = right; countCostRates++; - } else { + }else if(isReward(left)) { + rewardRate = right; + countRewardRates++; + }else { hasClockRates = true; if (!inforall) { invariant = invariant.empty() ? expr @@ -702,9 +710,13 @@ void TypeChecker::visitLocation(location_t& loc) decomposer.decompose(inv); inv = decomposer.invariant; loc.costRate = decomposer.costRate; + loc.rewardRate = decomposer.rewardRate; if (decomposer.countCostRates > 1) { handleError(inv, "$Only_one_cost_rate_is_allowed"); } + if (decomposer.countRewardRates > 1) { + handleError(inv, "$Only_one_reward_rate_is_allowed"); + } if (decomposer.hasClockRates) { doc.recordStopWatch(); } @@ -1930,7 +1942,7 @@ bool TypeChecker::checkExpression(expression_t expr) break; case RATE: - if (isCost(expr[0]) || isClock(expr[0])) { + if (isCost(expr[0]) || isReward(expr[0]) || isClock(expr[0])) { type = type_t::createPrimitive(RATE); } break; @@ -1947,7 +1959,7 @@ bool TypeChecker::checkExpression(expression_t expr) break; case ASSPLUS: - if ((!isInteger(expr[0]) && !isCost(expr[0])) || !isIntegral(expr[1])) { + if ((!isInteger(expr[0]) && !isCost(expr[0]) && !isReward(expr[0])) || !isIntegral(expr[1])) { handleError(expr, "$Increment_operator_can_only_be_used_for_integers_and_cost_variables"); } else if (!isModifiableLValue(expr[0])) { handleError(expr[0], "$Left_hand_side_value_expected");