<commit_before>"""
Tests for the abstraction from continuous dynamics to logic
"""
import logging
logging.basicConfig(level=logging.INFO)
logger = logging.getLogger(__name__)
#logging.getLogger('tulip').setLevel(logging.ERROR)
logger.setLevel(logging.DEBUG)

import numpy as np

from tulip import abstract, hybrid
import polytope as pc

input_bound = 0.4

def subsys0():
    dom = pc.box2poly([[0., 3.], [0., 2.]])
    
    A = np.eye(2)
    B = np.eye(2)
    
    U = pc.box2poly([[0., 1.],
                  [0., 1.]])
    U.scale(input_bound)
    
    sys_dyn = hybrid.LtiSysDyn(A, B, Uset=U, domain=dom)
    
    return sys_dyn

def subsys1():
    dom = pc.box2poly([[0., 3.], [0., 2.]])
    
    A = np.eye(2)
    B = np.eye(2)
    
    U = pc.box2poly([[0., 0.],
                  [-1., 0.]])
    U.scale(input_bound)
    
    sys_dyn = hybrid.LtiSysDyn(A, B, Uset=U, domain=dom)
    
    return sys_dyn

def transition_directions_test():
    """
    unit test for correctness of abstracted transition directions, with:
    
      - uni-directional control authority
      - no disturbance
    """
    modes = []
    modes.append(('normal', 'fly'))
    modes.append(('refuel', 'fly'))
    env_modes, sys_modes = zip(*modes)
    
    cont_state_space = pc.box2poly([[0., 3.], [0., 2.]])
    pwa_sys = dict()
    pwa_sys[('normal', 'fly')] = hybrid.PwaSysDyn(
        [subsys0()], cont_state_space
    )
    pwa_sys[('refuel', 'fly')] = hybrid.PwaSysDyn(
        [subsys1()], cont_state_space
    )
    
    switched_dynamics = hybrid.SwitchedSysDyn(
        disc_domain_size=(len(env_modes), len(sys_modes)),
        dynamics=pwa_sys,
        env_labels=env_modes,
        disc_sys_labels=sys_modes,
        cts_ss=cont_state_space
    )
    
    cont_props = {}
    cont_props['home'] = pc.box2poly([[0., 1.], [0., 1.]])
    cont_props['lot'] = pc.box2poly([[2., 3.], [1., 2.]])
    
    ppp = abstract.prop2part(cont_state_space, cont_props)
    ppp, new2old = abstract.part2convex(ppp)
    
    N = 8
    trans_len=1
    
    disc_params = {}
    for mode in modes:
        disc_params[mode] = {'N':N, 'trans_length':trans_len}
    
    swab = abstract.discretize_switched(
        ppp, switched_dynamics, disc_params,
        plot=True, show_ts=True, only_adjacent=False
    )
    
    ts = swab.modes[('normal', 'fly')].ts
    edges = {('s0', 's0'), ('s1', 's1'), ('s2', 's2'), ('s3', 's3'),
             ('s4', 's4'), ('s5', 's5'),
             ('s1', 's2'), ('s1', 's4'), ('s1', 's5'),
             ('s2', 's3'), ('s2', 's5'), ('s2', 's0'),
             ('s3', 's0'),
             ('s4', 's5'),
             ('s5', 's0')}
    
    logger.debug(set(ts.edges() ).symmetric_difference(edges) )
    assert(set(ts.edges() ) == edges)
    
    ts = swab.ts
    
    assert(set(ts.edges() ) == edges)
    for i, j in edges:
        assert(ts[i][j][0]['env_actions'] == 'normal')
        assert(ts[i][j][0]['sys_actions'] == 'fly')

transition_directions_test.slow = True

def test_transient_regions():
    """drift is too strong, so no self-loop must exist
    
    This bug caused when running union is taken between Presets
    during solve_feasible, as happened with old use_all_horizon,
    cf:
        - 5b1e9681918739b276a221fcc1fd6eebfd058ce3
        - f5f4934ab9d21062f633eef3861ad935c3d3b54b
    """
    dom = pc.box2poly([[0.0, 4.0], [0.0, 3.0]])
    
    def cont_predicates():
        p = dict()
        p['safe'] = pc.box2poly([[0.5, 3.5], [0.5, 2.5]])
        
        ppp = abstract.prop2part(dom, p)
        ppp, new2old_reg = abstract.part2convex(ppp)
        ppp.plot()
        return ppp
    
    def drifting_dynamics():
        A = np.array([[1.0, 0.0],
                      [0.0, 1.0]])<commit_msg>turn off plotting in tests<commit_after>"""
Tests for the abstraction from continuous dynamics to logic

if you want to use plotting over ssh, then use:

    ssh -X whatever
"""
import logging
logging.basicConfig(level=logging.INFO)
logger = logging.getLogger(__name__)
#logging.getLogger('tulip').setLevel(logging.ERROR)
logger.setLevel(logging.DEBUG)

import numpy as np

from tulip import abstract, hybrid
import polytope as pc

input_bound = 0.4

def subsys0():
    dom = pc.box2poly([[0., 3.], [0., 2.]])
    
    A = np.eye(2)
    B = np.eye(2)
    
    U = pc.box2poly([[0., 1.],
                  [0., 1.]])
    U.scale(input_bound)
    
    sys_dyn = hybrid.LtiSysDyn(A, B, Uset=U, domain=dom)
    
    return sys_dyn

def subsys1():
    dom = pc.box2poly([[0., 3.], [0., 2.]])
    
    A = np.eye(2)
    B = np.eye(2)
    
    U = pc.box2poly([[0., 0.],
                  [-1., 0.]])
    U.scale(input_bound)
    
    sys_dyn = hybrid.LtiSysDyn(A, B, Uset=U, domain=dom)
    
    return sys_dyn

def transition_directions_test():
    """
    unit test for correctness of abstracted transition directions, with:
    
      - uni-directional control authority
      - no disturbance
    """
    modes = []
    modes.append(('normal', 'fly'))
    modes.append(('refuel', 'fly'))
    env_modes, sys_modes = zip(*modes)
    
    cont_state_space = pc.box2poly([[0., 3.], [0., 2.]])
    pwa_sys = dict()
    pwa_sys[('normal', 'fly')] = hybrid.PwaSysDyn(
        [subsys0()], cont_state_space
    )
    pwa_sys[('refuel', 'fly')] = hybrid.PwaSysDyn(
        [subsys1()], cont_state_space
    )
    
    switched_dynamics = hybrid.SwitchedSysDyn(
        disc_domain_size=(len(env_modes), len(sys_modes)),
        dynamics=pwa_sys,
        env_labels=env_modes,
        disc_sys_labels=sys_modes,
        cts_ss=cont_state_space
    )
    
    cont_props = {}
    cont_props['home'] = pc.box2poly([[0., 1.], [0., 1.]])
    cont_props['lot'] = pc.box2poly([[2., 3.], [1., 2.]])
    
    ppp = abstract.prop2part(cont_state_space, cont_props)
    ppp, new2old = abstract.part2convex(ppp)
    
    N = 8
    trans_len=1
    
    disc_params = {}
    for mode in modes:
        disc_params[mode] = {'N':N, 'trans_length':trans_len}
    
    swab = abstract.discretize_switched(
        ppp, switched_dynamics, disc_params,
        plot=False, show_ts=True, only_adjacent=False
    )
    
    ts = swab.modes[('normal', 'fly')].ts
    edges = {('s0', 's0'), ('s1', 's1'), ('s2', 's2'), ('s3', 's3'),
             ('s4', 's4'), ('s5', 's5'),
             ('s1', 's2'), ('s1', 's4'), ('s1', 's5'),
             ('s2', 's3'), ('s2', 's5'), ('s2', 's0'),
             ('s3', 's0'),
             ('s4', 's5'),
             ('s5', 's0')}
    
    logger.debug(set(ts.edges() ).symmetric_difference(edges) )
    assert(set(ts.edges() ) == edges)
    
    ts = swab.ts
    
    assert(set(ts.edges() ) == edges)
    for i, j in edges:
        assert(ts[i][j][0]['env_actions'] == 'normal')
        assert(ts[i][j][0]['sys_actions'] == 'fly')

transition_directions_test.slow = True

def test_transient_regions():
    """drift is too strong, so no self-loop must exist
    
    This bug caused when running union is taken between Presets
    during solve_feasible, as happened with old use_all_horizon,
    cf:
        - 5b1e9681918739b276a221fcc1fd6eebfd058ce3
        - f5f4934ab9d21062f633eef3861ad935c3d3b54b
    """
    dom = pc.box2poly([[0.0, 4.0], [0.0, 3.0]])
    
    def cont_predicates():
        p = dict()
        p['safe'] = pc.box2poly([[0.5, 3.5], [0.5, 2.5]])
        
        ppp = abstract.prop2part(dom, p)
        ppp, new2old_reg = abstract.part2convex(ppp)
        #ppp.plot()
        return ppp
    
    def drifting_dynamics():
        A = np.array([[1.0, 0.0],
                      [0.0, 1.0]])
{'fraction_non_alphanumeric': 0.17221706249170757, 'fraction_numerical': 0.0424572110919464, 'mean_word_length': 2.3878651685393257, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, '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': '4190443', 'n_tokens_mistral': 3013, 'n_tokens_neox': 2859, 'n_words': 574}