From 08096254ecf8c2341320e255ad74a7d99fb46d47 Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex.auvolat@ansys.com>
Date: Wed, 2 Jul 2014 10:27:30 +0200
Subject: More verbosity ; adapt rfollow so that it can be proved

---
 tests/source/rfollow.scade | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'tests')

diff --git a/tests/source/rfollow.scade b/tests/source/rfollow.scade
index 6ee1558..c62c90d 100644
--- a/tests/source/rfollow.scade
+++ b/tests/source/rfollow.scade
@@ -1,14 +1,16 @@
 node follow(a: real) returns (probe f: real)
 var
   probe pf: real;
+  prop: bool;
 let
   assume h1: a >= 0. and a <= 1.;
-  guarantee g1: f >= 0. and f <= 1.;
-  guarantee g2: pf >= 0. and pf <= 1.;
 
   pf = 0. -> pre f;
   f = (pf + a) / 2.0;
 
+  prop = (f >= 0 and f <= 1.);
+
+  guarantee g1: (true -> pre prop) and prop;
 tel
 
 
-- 
cgit v1.2.3