From c65b0c7ba4f8f500387fc943ed659e63fb4181f8 Mon Sep 17 00:00:00 2001 From: alex Date: Tue, 12 Dec 2017 00:20:13 -0800 Subject: [PATCH] better version --- examples/OneOf.cpp | 59 +++++++++++++++++++++++++++++++++------------- 1 file changed, 43 insertions(+), 16 deletions(-) diff --git a/examples/OneOf.cpp b/examples/OneOf.cpp index c38fc5b..893e49d 100644 --- a/examples/OneOf.cpp +++ b/examples/OneOf.cpp @@ -18,26 +18,53 @@ using namespace deepstate; - +#define LENGTH 3 TEST(OneOfExample, ProduceSixtyOrHigher) { - symbolic_int x; - - ASSUME_LT(x, 5); - - int N = 3; - - while (N > 0) { - N--; + symbolic_int start; + ASSUME_LT(start, 5); + int x = start; + + // char choices[LENGTH+1]; + + // Add this back in and uncomment out choices parts below, add + // & choices, N to captures, and it becomes quite difficult. + + int N = 0; + while (N < LENGTH) { + N++; OneOf( - [&x] {x += 1; printf("-1\n");}, - [&x] {x -= 1; printf("+1\n");}, - [&x] {x *= 2; printf("*2\n");}, - [&x] {x += 10; printf("+=10\n");}, - [&x] {x = 0; printf("=0\n");}); - + [&x] { + x += 1; + printf("-1\n"); + //choices[N] = '+'; + }, + [&x] { + x -= 1; + printf("+1\n"); + //choices[N] = '-'; + }, + [&x] { + x *= 2; + printf("*2\n"); + //choices[N] = '2'; + }, + [&x] { + x += 10; + printf("+=10\n"); + //choices[N] = 'x'; + }, + [&x] { + x = 0; + printf("=0\n"); + //choices[N] = '0'; + }); + + //choices[N+1] = 0; ASSERT_LE(x, 60) - << x << " is >= 60!"; + << x << " is >= 60: " << + //" did " << choices << + " from " << start; } }