DeforaNetworks/deepstate
3
0
Fork 0
Code Releases Activity

Version that works, test depth

Browse Source
This commit is contained in:
alex 2017-12-11 23:17:18 -08:00
parent 669f6cf3f9
commit 70090bd712
1 changed files with 13 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

21
examples/OneOf.cpp
View File

@ -23,17 +23,22 @@ using namespace deepstate;
TEST(OneOfExample, ProduceSixtyOrHigher) {
symbolic_int x;
ASSUME_LT(x, 3);
while (1) {
ASSUME_LT(x, 5);
int N = 3;
while (N > 0) {
N--;
OneOf(
[&x] {x += 1; printf("-1\n");},
[&x] {x -= 1; printf("+1\n");},
[&x] {x *= 2; printf("*2\n");},
[&x] {x = 0; printf("=0\n");});
[&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");});
ASSERT_LE(x, 60)
<< x << " is sixty!";
};
<< x << " is >= 60!";
}
}
int main(int argc, char *argv[]) {