PyUPPAAL icon indicating copy to clipboard operation
PyUPPAAL copied to clipboard

更新SimTrace功能的描述

Open Jack0Chan opened this issue 3 years ago • 0 comments

印象中对于SimTrace的过滤功能好像没有案例或者描述之类的,看看能不能补上。下面是需要考虑的点。

FilterByAction

You can filter specific edges with specific actions.

FilterByClock

You can filter constraints with specific clocks (e.g. gclk).

Constraints with certain clocks:
t1
t1 or t2 or t3
t1 and t2
t1 or (t3 and t4)
'or' means exist one in DBM form.
'and' means both in DBM form.
For example:
DBM = 
 [(t1, t2, True, 100), 
   (t1, t3, True, 500), 
   (t2, t4, True, 200),
   (t3, t4, True, 300)]
t1 will filter: 
 [(t1, t2, True, 100), 
   (t1, t3, True, 500), 
   (t2, t4, True, 200),
   (t3, t4, True, 300)]
t1 or t2 or t3 will filter:
 [(t1, t2, True, 100), 
 (t1, t3, True, 500), 
 (t2, t4, True, 200),
 (t3, t4, True, 300)]
t1 and t2 will filter:
 [(t1, t2, True, 100), 
   (t1, t3, True, 500), 
   (t2, t4, True, 200),
   (t3, t4, True, 300)]
t1 or (t3 and t4) will filter:
 [(t1, t2, True, 100), 
   (t1, t3, True, 500), 
   (t2, t4, True, 200),
   (t3, t4, True, 300)]
(t1 and t2 and t3) or t4
S = [t1, t2, t3], [t1, t2, t3, *]

(t1 and t2) or (t1 and t3) or (t2 and t3)

find (exp1, exp2) \in S*S
exp1 * exp2 \subset S*S

Action Pattern (Untime)

In most conditions, experts are concerned more about the sequence of the events than the exact clock constraints. Pattern is the sequence of focused actions without clock constraints. Due to the partial observations, there are different patterns that can explain the current features. In the pipes examples, there are two different paths that can lead to exit2. Pattern = Untime(Trace) All patterns.

Jack0Chan avatar Dec 15 '22 03:12 Jack0Chan