From fee760b5c08afa9c81b5f28b35afd3514f643770 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Thu, 10 Jul 2014 10:58:56 +0200 Subject: Fix a few things, this doesn't work well. --- tests/source/half.scade | 2 +- tests/source/updown2.scade | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'tests') diff --git a/tests/source/half.scade b/tests/source/half.scade index 541e81c..7e0df60 100644 --- a/tests/source/half.scade +++ b/tests/source/half.scade @@ -25,5 +25,5 @@ let c = a - b; guarantee c_bounded: c >= 0 and c <= 1; - guarantee link_c_half: (half and c = 1) or ((not half) and c = 0); + guarantee link_c_half: if half then (c = 1) else (c = 0); tel diff --git a/tests/source/updown2.scade b/tests/source/updown2.scade index 29c34ff..72d5bed 100644 --- a/tests/source/updown2.scade +++ b/tests/source/updown2.scade @@ -30,7 +30,7 @@ let guarantee y_bounded: y >= -bound and y <= bound; z = x + y; - guarantee x_y_opp: z = 0 and (true -> pre (z = 0)); + guarantee x_y_opp: z = 0; tel node test(i: int) returns(a, b, c: int; exit: bool) -- cgit v1.2.3