Costreward

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)

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

include/utap/common.h

@@ -236,6 +236,7 @@ namespace UTAP
             LOCATION_EXPR,
             CHANNEL,
             COST,
+            REWARD,
             INVARIANT,
             INVARIANT_WR,
             GUARD,

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;
     };

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); }
 

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
 }
 

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:

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");