#!/usr/bin/env python
"""
Based on test code moved here from bottom of tulip/jtlvint.py

SCL; 5 Sep 2011.
Vasu Raman; 4 Sept 2013
"""

import os

from tulip.spec import GRSpec
from tulip.jtlvint import *


def test_dumpjtlv():
    spec = GRSpec(env_vars="x", sys_vars="y",
                  env_init="x", env_prog="x",
                  sys_init="y", sys_safety=["y -> !next(y)", "!y -> next(y)"],
                  sys_prog="y & x")
    specLTL = spec.to_jtlv()
    assumption = specLTL[0]
    guarantee = specLTL[1]
    assert check_gr1(assumption, guarantee, spec.env_vars.keys(), spec.sys_vars.keys())

def test_check_realizable():
    spec = GRSpec(env_vars="x", sys_vars="y",
                  env_init="x", env_prog="x",
                  sys_init="y", sys_safety=["y -> !next(y)", "!y -> next(y)"],
                  sys_prog="y & x")
    assert not check_realizable(spec)
    spec.sys_safety = []
    assert check_realizable(spec)

def test_synthesize():
    spec = GRSpec(env_vars="x", sys_vars="y",
                  env_init="x", env_prog="x",
                  sys_init="y",
                  sys_prog=["y & x", "!y"])
    aut = synthesize(spec)
    assert aut is not None

@@ -23,69 +23,37 @@
 %22%22%22%0A
-Based on test code moved here from bottom of tulip/jtlvint.py
+Test the interface with JTLV.
 %0A%0ASC
@@ -64,17 +64,17 @@
  Sep 201
-1
+3
 .%0AVasu R

TEST DOC: Correct date of previous commit; defunct historical reference