from formula to counterexample
assertion
all s, s’ | pre (s) ? proc (s,s’) -> post (s, s’)
negate
some s, s’ | pre (s) ? proc (s,s’) ? ! post (s, s’)
proc (s, s’) is
F (s,s’) ; G (s, s’) ; H (s, s’)
desugar ;
some s1| ((some s0 | F(s, s0) ? G (s0, s1)) ? H (s1, s’)
skolemize
pre (s) ? F (s, s0) ? G (s0, s1) ? H (s1, s’) ? ! post (s, s’)
now find model in finite scope
obtain counterexample <s, s0, s1, s’>