Skip to content

Commit 41a15a5

Browse files
authored
Merge pull request #1203 from diffblue/smv_ltlspec_or1
SMV: test for LTL property with 'or'
2 parents 955c752 + 2d5d97e commit 41a15a5

File tree

2 files changed

+13
-0
lines changed

2 files changed

+13
-0
lines changed
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
smv_ltlspec_or1.smv
3+
--bound 10
4+
^\[spec1\] F !x \| G x: PROVED up to bound 10$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
MODULE main
2+
3+
VAR x : boolean;
4+
5+
LTLSPEC (F !x) | G x

0 commit comments

Comments
 (0)