SPARKS pseudocode
input bool x12
input bool x13
input bool x14
input bool x23
input bool x24
input bool x34
output bool w
if x12 and x34 then
return w @ 1
endif
if x13 and x24 then
return w @ 1
endif
if x14 and x23 then
return w @ 1
endif
return w @ 0
SPARKS pseudo-assembly
. input bool x12
. input bool x13
. input bool x14
. input bool x23
. input bool x24
. input bool x34
. output bool w
. set guard0 and x12 x34
. set guard0 not guard0
. if guard0 else0
1 return w copy 1
else0 nop
. set guard2 and x13 x24
. set guard2 not guard2
. if guard2 else2
3 return w copy 1
else2 nop
. set guard4 and x14 x23
. set guard4 not guard4
. if guard4 else4
5 return w copy 1
else4 nop
6 return w copy 0
Parameter file
word_size=2
time_bound=24
Generated LP
Sample yes instance
# count = 14
param d['w'] := 0;
param c :=
'x12' -2
'x13' 2
'x14' 2
'x23' 2
'x24' -2
'x34' -2
;
Sample no instance
# count = 56
param d['w'] := 0;
param c :=
'x12' -2
'x13' -2
'x14' -2
'x23' 2
'x24' 2
'x34' 2
;