From 6966f2fffe590256da84291630b5cc6d6eda289b Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Wed, 10 Aug 2016 22:00:31 +0200
Subject: [PATCH] fix sign to be as in jani, add truncate

Former-commit-id: 9bdfa8f9fa64a573d3534e3886b650086031630e [formerly 48e15d50705eafd1ec18246ed3d846710e894add]
Former-commit-id: 298d46b5cc4c0dbc9979b7963e075442870c8c38
---
 src/storage/expressions/Expression.cpp | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp
index 66d5635ff..3d6094d8b 100644
--- a/src/storage/expressions/Expression.cpp
+++ b/src/storage/expressions/Expression.cpp
@@ -316,18 +316,17 @@ namespace storm {
 
         Expression abs(Expression const& first) {
             STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Abs is only defined for numerical operands");
-            return ite(first < first.getManager().integer(0), -first, first);
+            return ite(first < 0, -first, first);
         }
 
         Expression sign(Expression const& first) {
             STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Sign is only defined for numerical operands");
-            return ite(first < 0, -first, first);
+            return ite(first > 0, first.getManager().integer(1), ite(first < 0, first.getManager().integer(0), first.getManager().integer(0)));
         }
 
         Expression truncate(Expression const& first) {
             STORM_LOG_THROW(first.hasNumericalType(), storm::exceptions::InvalidTypeException, "Truncate is only defined for numerical operands");
-            // TODO implement (via Ite?)
-            STORM_LOG_ERROR("Not yet implemented");
+            return ite(first < 0, floor(first), ceil(first));
         }
 
         Expression disjunction(std::vector<storm::expressions::Expression> const& expressions) {