← Back to branch summary

~yrke/opaal/timedart-vars

« back to all changes in this revision

Viewing changes to opaal/model_parsers/pyuppaal/successor_generator.py

  • Committer: Kenneth Yrke Joergensen
  • Date: 2011-05-02 06:09:06 UTC
  • Revision ID: kenneth@yrke.dk-20110502060906-i2cpgs2vnsa76w73
now returns sucessor states

Show diffs side-by-side

added added

removed removed

Lines of Context:
opaal/model_parsers/pyuppaal/successor_generator.py
189
189
        #print "Transitions:"
190
190
        #print self.transitions
191
191
 
192
 
    def checkInvariant(self, state):
193
 
        for t_idx in self.invariants.keys():
194
 
            cur_inv = self.invariants[t_idx][state.locs[t_idx]]
195
 
            if cur_inv != '' and not eval(cur_inv, self.constants, state):
196
 
                return False
197
 
        return True
 
192
#    def checkInvariant(self, a):
 
193
#        state,_ = a
 
194
#        for t_idx in self.invariants.keys():
 
195
#            cur_inv = self.invariants[t_idx][state.locs[t_idx]]
 
196
#            if cur_inv != '' and not eval(cur_inv, self.constants, state):
 
197
#                return False
 
198
#        return True
198
199
 
199
200
 
200
201
    def normalize(self, state, w):
201
 
        min = 12
202
 
        for c in self.clocks:
203
 
            state[c] = min(w+state[c], 12)
204
 
            if state[c] <= min:
205
 
                min = state[c]
 
202
        m = 12
 
203
        for c,_ in self.clocks:
 
204
            state[c] = min([w+state[c], 12])
 
205
            if state[c] <= m:
 
206
                m = state[c]
206
207
 
207
208
        #TODO: We dont need to update if no changes has been made
208
209
        
209
 
        for c in self.clocks:
210
 
            state[c] = state[c] - min   
 
210
        for c,_ in self.clocks:
 
211
            state[c] = state[c] - m
211
212
 
212
 
        return (state, min)
 
213
        return (state, m)
213
214
 
214
215
    def trans_successors(self, state, trans_info=False):
215
216
        #Take an active transition
217
218
            for (target_idx, guard, update, sync, debug_info, lowerVal, higherVal) in self.transitions[t_idx][state.locs[t_idx]]:
218
219
                #Evaluate guard
219
220
 
220
 
                print lowerVal
221
 
                print higherVal
222
 
                #Find min and max delay for each clocks 
223
 
                start = 0
224
 
                for c,_ in self.clocks:
225
 
                    guard = 0
 
221
                w = self.pwlist.getW(state)
 
222
                print lowerVal
 
223
                print higherVal
 
224
                        #Find min and max delay for each clocks 
 
225
                start = 0
 
226
                for c,_ in self.clocks:
 
227
                    guard = 0
226
228
                    try:
227
 
                        guard = lowerVal[c]
228
 
                    except Exception, e:
229
 
                        continue #No lower guard set, is enabled from now
230
 
                    print "guard: ",  guard
 
229
                        guard = lowerVal[c]
 
230
                    except Exception, e:
 
231
                        continue #No lower guard set, is enabled from now
 
232
                    print "guard: ",  guard
231
233
                    if guard > start:
232
234
                        start = guard
233
 
                print start
234
 
 
235
 
                end = 12
236
 
                for c,_ in self.clocks:
237
 
                    guard = 0
 
235
                print start
 
236
        
 
237
                end = 12
 
238
                for c,_ in self.clocks:
 
239
                    guard = 0
238
240
                    try:
239
 
                        guard = higherVal[c]
240
 
                    except Exception, e:
241
 
                        continue #No lower guard set, is enabled from now
242
 
 
243
 
                    print "guard: ",  guard
244
 
                    print guard, end, guard < end
 
241
                        guard = higherVal[c]
 
242
                    except Exception, e:
 
243
                        continue #No lower guard set, is enabled from now
 
244
        
 
245
                    print "guard: ",  guard
 
246
                    print guard, end, guard < end
245
247
                    if guard < end:
246
248
                        end = guard
247
 
                print end
248
 
 
249
 
                #Check if the guard can be satisfied 
250
 
 
251
 
                a = state.copy()
 
249
                print end
 
250
        
 
251
                #Check if the guard can be satisfied 
 
252
                if start > end or w > end:
 
253
                    return
 
254
        
 
255
                #Calculate discrete update
 
256
                a = state.copy()
252
257
                a.locs[t_idx] = target_idx
253
 
 
254
 
                yield a
 
258
                #Calculate successor states
 
259
                if update == None:
 
260
                    yield self.normalize(a, w) # We only need to normalize if we had a open higher guard
 
261
                else: #yield many states
 
262
                    for i in range(start, end+1): #dont need infin as max is mc+1
 
263
                        yield self.normalize(a,i) #not clever as we use normalize to calculate the state
255
264
 
256
265
#               #Check the guard using the values
257
266
#                if guard == None or self.satesfyguard(state, lowerVal, higherVal):
320
329
 
321
330
    def successors(self, state):
322
331
        for a in self.trans_successors(state):
323
 
            if self.checkInvariant(a):
324
 
                yield a
 
332
            #if self.checkInvariant(a):
 
333
            yield a
325
334
        #for a in self.delay_successors_1step(state):
326
335
        #    if self.checkInvariant(a):
327
336
        #        yield a