<commit_before>#!/usr/bin/env python
"""
Test the interface with gr1c.

SCL; 25 Feb 2012.
"""

import os

from tulip.spec import GRSpec
from tulip.gr1cint import *


REFERENCE_SPECFILE = """
ENV: x;
SYS: y;

ENVINIT: x;
ENVTRANS:;# [](x -> !x') & [](!x -> x');
ENVGOAL: []<>x;

# Blank lines are optional and can placed between sections or parts of
# formulas.

SYSINIT: y;

SYSTRANS: # Notice the safety formula spans two lines.
[](y -> !y')
& [](!y -> y');

SYSGOAL: []<>y&x;
"""


class gr1cint_test:

    def setUp(self):
        pass

    def tearDown(self):
        pass

    def test_check_syntax(self):
        assert check_syntax(REFERENCE_SPECFILE, verbose=1)
        assert not check_syntax("foo", verbose=1)

    def test_dumpgr1c(self):
        spec = GRSpec(env_vars="x", sys_vars="y",
                      env_init="x", env_prog="x",
                      sys_init="y", sys_safety=["y -> !y'", "!y -> y'"],
                      sys_prog="y & x")
        assert check_syntax(spec.dumpgr1c(), verbose=1)

    def test_check_realizable(self):
        spec = GRSpec(env_vars="x", sys_vars="y",
                      env_init="x", env_prog="x",
                      sys_init="y", sys_safety=["y -> !y'", "!y -> y'"],
                      sys_prog="y & x")
        assert not check_realizable(spec)
        spec.sys_safety = []
        assert check_realizable(spec)<commit_msg>New small unit test for synthesis with gr1c.<commit_after>#!/usr/bin/env python
"""
Test the interface with gr1c.

SCL; 11 Mar 2012.
"""

import os

from tulip.conxml import loadXML
from tulip.spec import GRSpec
from tulip.gr1cint import *


REFERENCE_SPECFILE = """
ENV: x;
SYS: y;

ENVINIT: x;
ENVTRANS:;# [](x -> !x') & [](!x -> x');
ENVGOAL: []<>x;

# Blank lines are optional and can placed between sections or parts of
# formulas.

SYSINIT: y;

SYSTRANS: # Notice the safety formula spans two lines.
[](y -> !y')
& [](!y -> y');

SYSGOAL: []<>y&x;
"""

REFERENCE_AUTXML = """<?xml version="1.0" encoding="UTF-8"?>
<tulipcon xmlns="http://tulip-control.sourceforge.net/ns/0" version="0">
  <spec><env_init></env_init><env_safety></env_safety><env_prog></env_prog><sys_init></sys_init><sys_safety></sys_safety><sys_prog></sys_prog></spec>
  <aut>
    <node>
      <id>0</id><name></name>
      <child_list> 1 2</child_list>
      <state>
        <item key="x" value="1" />
        <item key="y" value="0" />
      </state>
    </node>
    <node>
      <id>1</id><name></name>
      <child_list> 1 2</child_list>
      <state>
        <item key="x" value="0" />
        <item key="y" value="0" />
      </state>
    </node>
    <node>
      <id>2</id><name></name>
      <child_list> 1 0</child_list>
      <state>
        <item key="x" value="1" />
        <item key="y" value="1" />
      </state>
    </node>
  </aut>
  <extra></extra>
</tulipcon>
"""


class gr1cint_test:

    def setUp(self):
        pass

    def tearDown(self):
        pass

    def test_check_syntax(self):
        assert check_syntax(REFERENCE_SPECFILE, verbose=1)
        assert not check_syntax("foo", verbose=1)

    def test_dumpgr1c(self):
        spec = GRSpec(env_vars="x", sys_vars="y",
                      env_init="x", env_prog="x",
                      sys_init="y", sys_safety=["y -> !y'", "!y -> y'"],
                      sys_prog="y & x")
        assert check_syntax(spec.dumpgr1c(), verbose=1)

    def test_check_realizable(self):
        spec = GRSpec(env_vars="x", sys_vars="y",
                      env_init="x", env_prog="x",
                      sys_init="y", sys_safety=["y -> !y'", "!y -> y'"],
                      sys_prog="y & x")
        assert not check_realizable(spec)
        spec.sys_safety = []
        assert check_realizable(spec)
        
    def test_synthesize(self):
        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
        (prob, sys_dyn, aut_ref) = loadXML(REFERENCE_AUTXML)
        assert aut == aut_ref
{'fraction_non_alphanumeric': 0.1713176413491871, 'fraction_numerical': 0.011890317884008735, 'mean_word_length': 2.3349514563106797, 'pattern_counts': {'":': 0, '<': 64, '<?xml version=': 1, '>': 80, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 3}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7210457', 'n_tokens_mistral': 1556, 'n_tokens_neox': 1464, 'n_words': 323}