import spot
import spot.ltsmin
import tempfile
import shutil
import sys

# this test requires divine with --ltsmin support
if shutil.which("divine") == None:
    sys.exit(77)
import subprocess
out = subprocess.check_output(['divine', 'compile',
                               '--help'], stderr=subprocess.STDOUT)
if b'LTSmin' not in out:
    sys.exit(77)

# the test case actually starts here
with tempfile.NamedTemporaryFile(dir='.', suffix='.dve') as fp:
    fp.write(b"""int f = 3;
process R {
  int p = 1, found = 0;
  state i, e;
  init i;
  trans
    i -> i {guard p != f; effect p = p + 1;},
    i -> e {guard p == f; effect found = 1;},
    e -> e {};
}
system async;
""")
    fp.flush()
    m = spot.ltsmin.load(fp.name)

    def modelcheck(formula, model):
        a = spot.translate(formula)
        k = m.kripke([ap.ap_name() for ap in a.ap()])
        p = spot.otf_product(k, a)
        return p.is_empty()

    assert(modelcheck('X "R.found"', m) == True)