utils.py 7.98 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

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

    """
li213's avatar
li213 committed
68
69
    # random.seed(4)

navidmokh's avatar
navidmokh committed
70
71
72
73
74
75
76
77
    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))]

78

navidmokh's avatar
navidmokh committed
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
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"
97
98
    return [(upper[i] - lower[i]) / 2 for i in range(len(upper))]

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

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"
118
119
    return [(upper[i] + lower[i]) / 2 for i in range(len(upper))]

navidmokh's avatar
navidmokh committed
120
121
122
123
124
125
126

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

    Returns:
131
        str: a string to represent a mode
navidmokh's avatar
navidmokh committed
132
133

    """
134
135
    return g.vs[vertex]['label'] + ',' + str(vertex)

navidmokh's avatar
navidmokh committed
136

137
def handleReplace(input_str, keys):
navidmokh's avatar
navidmokh committed
138
139
140
141
142
143
144
145
146
    """
    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:
147
        input_str (str): original string need to be replaced
navidmokh's avatar
navidmokh committed
148
149
150
        keys (list): list of variable strings

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

    """
    idxes = []
    i = 0
156
    original = input_str
navidmokh's avatar
navidmokh committed
157

158
    keys.sort(key=lambda s: len(s))
navidmokh's avatar
navidmokh committed
159
    for key in keys[::-1]:
160
161
162
163
        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
164
165
166

    idxes = sorted(idxes)

167
    input_str = original
navidmokh's avatar
navidmokh committed
168
    for idx in idxes[::-1]:
169
170
171
172
173
        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
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190

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

    """
191
192
    return 'Not(' + orig + ')'

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

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

216

navidmokh's avatar
navidmokh committed
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
262
263
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"

264

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

278

navidmokh's avatar
navidmokh committed
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
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"]