utils.py 7.95 KB
Newer Older
navidmokh's avatar
navidmokh committed
1
2
3
4
5
6
7
8
9
10
11
12
"""
This file contains common utils for DryVR
"""

import importlib
import random

from collections import namedtuple

# This is the tuple for input file parsed by DryVR
DryVRInput = namedtuple(
    'DryVRInput',
13
14
    'vertex edge guards variables initialSet unsafeSet timeHorizon path resets initialVertex deterministic '
    'bloatingMethod kvalue '
navidmokh's avatar
navidmokh committed
15
16
17
18
19
20
21
22
)

# This is the tuple for rtt input file parsed by DryVR
RrtInput = namedtuple(
    'RttInput',
    'modes variables initialSet unsafeSet goalSet timeHorizon minTimeThres path goal bloatingMethod kvalue'
)

23

navidmokh's avatar
navidmokh committed
24
25
26
27
28
29
30
31
32
def importSimFunction(path):
    """
    Load simulation function from given file path
    Note the folder in the examples directory must have __init__.py
    And the simulation function must be named TC_Simulate
    The function should looks like following:
        TC_Simulate(Mode, initialCondition, time_bound)
    
    Args:
33
        path (str): Simulator directory.
navidmokh's avatar
navidmokh committed
34
35
36
37
38
39

    Returns:
        simulation function

    """
    try:
40
41
42
43
44
45
46
        # FIXME TC_Simulate should just be a simple call back function
        import os
        import sys
        sys.path.append(os.path.abspath(path))
        mod_name = path.replace('/', '.')
        module = importlib.import_module(mod_name)
        sys.path.pop()
47

48
49
50
51
52
        return module.TC_Simulate
    except ImportError as e:
        print("Import simulation function failed!")
        print(e)
        exit()  # TODO Proper return
navidmokh's avatar
navidmokh committed
53

54

navidmokh's avatar
navidmokh committed
55
56
57
58
59
60
def randomPoint(lower, upper):
    """
    Pick a random point between lower and upper bound
    This function supports both int or list
    
    Args:
61
62
        lower (list or int or float): lower bound.
        upper (list or int or float): upper bound.
navidmokh's avatar
navidmokh committed
63
64
65
66
67
68
69
70
71
72
73
74
75

    Returns:
        random point (either float or list of float)

    """
    if isinstance(lower, int) or isinstance(lower, float):
        return random.uniform(lower, upper)

    if isinstance(lower, list):
        assert len(lower) == len(upper), "Random Point List Range Error"

        return [random.uniform(lower[i], upper[i]) for i in range(len(lower))]

76

navidmokh's avatar
navidmokh committed
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
def calcDelta(lower, upper):
    """
    Calculate the delta value between the lower and upper bound
    The function only supports list since we assue initial set is always list
    
    Args:
        lower (list): lowerbound.
        upper (list): upperbound.

    Returns:
        delta (list of float)

    """
    # Convert list into float in case they are int
    lower = [float(val) for val in lower]
    upper = [float(val) for val in upper]

    assert len(lower) == len(upper), "Delta calc List Range Error"
95
96
    return [(upper[i] - lower[i]) / 2 for i in range(len(upper))]

navidmokh's avatar
navidmokh committed
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115

def calcCenterPoint(lower, upper):
    """
    Calculate the center point between the lower and upper bound
    The function only supports list since we assue initial set is always list
    
    Args:
        lower (list): lowerbound.
        upper (list): upperbound.

    Returns:
        delta (list of float)

    """

    # Convert list into float in case they are int
    lower = [float(val) for val in lower]
    upper = [float(val) for val in upper]
    assert len(lower) == len(upper), "Center Point List Range Error"
116
117
    return [(upper[i] + lower[i]) / 2 for i in range(len(upper))]

navidmokh's avatar
navidmokh committed
118
119
120
121
122
123
124

def buildModeStr(g, vertex):
    """
    Build a unique string to represent a mode
    This should be something like "modeName,modeNum"
    
    Args:
125
126
        g (igraph.Graph): Graph object.
        vertex (int or str): vertex number.
navidmokh's avatar
navidmokh committed
127
128

    Returns:
129
        str: a string to represent a mode
navidmokh's avatar
navidmokh committed
130
131

    """
132
133
    return g.vs[vertex]['label'] + ',' + str(vertex)

navidmokh's avatar
navidmokh committed
134

135
def handleReplace(input_str, keys):
navidmokh's avatar
navidmokh committed
136
137
138
139
140
141
142
143
144
    """
    Replace variable in inputStr to self.varDic["variable"]
    For example:
        input
            And(y<=0,t>=0.2,v>=-0.1)
        output: 
            And(self.varDic["y"]<=0,self.varDic["t"]>=0.2,self.varDic["v"]>=-0.1)
    
    Args:
145
        input_str (str): original string need to be replaced
navidmokh's avatar
navidmokh committed
146
147
148
        keys (list): list of variable strings

    Returns:
149
        str: a string that all variables have been replaced into a desire form
navidmokh's avatar
navidmokh committed
150
151
152
153

    """
    idxes = []
    i = 0
154
    original = input_str
navidmokh's avatar
navidmokh committed
155

156
    keys.sort(key=lambda s: len(s))
navidmokh's avatar
navidmokh committed
157
    for key in keys[::-1]:
158
159
160
161
        for i in range(len(input_str)):
            if input_str[i:].startswith(key):
                idxes.append((i, i + len(key)))
                input_str = input_str[:i] + "@" * len(key) + input_str[i + len(key):]
navidmokh's avatar
navidmokh committed
162
163
164

    idxes = sorted(idxes)

165
    input_str = original
navidmokh's avatar
navidmokh committed
166
    for idx in idxes[::-1]:
167
168
169
170
171
        key = input_str[idx[0]:idx[1]]
        target = 'self.varDic["' + key + '"]'
        input_str = input_str[:idx[0]] + target + input_str[idx[1]:]
    return input_str

navidmokh's avatar
navidmokh committed
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188

def neg(orig):
    """
    Neg the original condition
    For example:
        input
            And(y<=0,t>=0.2,v>=-0.1)
        output: 
            Not(And(y<=0,t>=0.2,v>=-0.1))
    
    Args:
        orig (str): original string need to be neg

    Returns:
        a neg condition string

    """
189
190
    return 'Not(' + orig + ')'

navidmokh's avatar
navidmokh committed
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213

def trimTraces(traces):
    """
    trim all traces to the same length
    
    Args:
        traces (list): list of traces generated by simulator
    Returns:
        traces (list) after trim to the same length

    """

    ret_traces = []
    trace_lengths = []
    for trace in traces:
        trace_lengths.append(len(trace))
    trace_len = min(trace_lengths)

    for trace in traces:
        ret_traces.append(trace[:trace_len])

    return ret_traces

214

navidmokh's avatar
navidmokh committed
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
def checkVerificationInput(data):
    """
    Check verification input to make sure it is valid
    
    Args:
        data (obj): json data object
    Returns:
        None

    """
    assert len(data['variables']) == len(data['initialSet'][0]), "Initial set dimension mismatch"

    assert len(data['variables']) == len(data['initialSet'][1]), "Initial set dimension mismatch"

    assert len(data['edge']) == len(data["guards"]), "guard number mismatch"

    assert len(data['edge']) == len(data["resets"]), "reset number mismatch"

    if data["bloatingMethod"] == "PW":
        assert 'kvalue' in data, "kvalue need to be provided when bloating method set to PW"

    for i in range(len(data['variables'])):
        assert data['initialSet'][0][i] <= data['initialSet'][1][i], "initial set lowerbound is larger than upperbound"


def checkSynthesisInput(data):
    """
    Check Synthesis input to make sure it is valid
    
    Args:
        data (obj): json data object
    Returns:
        None

    """
    assert len(data['variables']) == len(data['initialSet'][0]), "Initial set dimension mismatch"

    assert len(data['variables']) == len(data['initialSet'][1]), "Initial set dimension mismatch"

    for i in range(len(data['variables'])):
        assert data['initialSet'][0][i] <= data['initialSet'][1][i], "initial set lowerbound is larger than upperbound"

    assert data["minTimeThres"] < data["timeHorizon"], "min time threshold is too large!"

    if data["bloatingMethod"] == "PW":
        assert 'kvalue' in data, "kvalue need to be provided when bloating method set to PW"

262

navidmokh's avatar
navidmokh committed
263
264
265
266
267
def isIpynb():
    """
    Check if the code is running on Ipython notebook
    """
    try:
268
        cfg = get_ipython().config
navidmokh's avatar
navidmokh committed
269
270
271
272
273
274
275
        if "IPKernelApp" in cfg:
            return True
        else:
            return False
    except NameError:
        return False

276

navidmokh's avatar
navidmokh committed
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
def overloadConfig(configObj, userConfig):
    """
    Overload user config to config module
    
    Args:
        configObj (module): config module
        userConfig (dict): user specified config
    """

    if "SIMUTESTNUM" in userConfig:
        configObj.SIMUTESTNUM = userConfig["SIMUTESTNUM"]

    if "SIMTRACENUM" in userConfig:
        configObj.SIMTRACENUM = userConfig["SIMTRACENUM"]

    if "REFINETHRES" in userConfig:
        configObj.REFINETHRES = userConfig["REFINETHRES"]

    if "CHILDREFINETHRES" in userConfig:
        configObj.CHILDREFINETHRES = userConfig["CHILDREFINETHRES"]

    if "RANDMODENUM" in userConfig:
        configObj.RANDMODENUM = userConfig["RANDMODENUM"]

    if "RANDSECTIONNUM" in userConfig:
        configObj.RANDSECTIONNUM = userConfig["RANDSECTIONNUM"]