ModelInference / synoptic

Inferring models of systems from observations of their behavior
Other
83 stars 25 forks source link

Document how log origin and FSM type impact invariants and model #370

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago
Logs could be created in two different ways: an event could be logged as it's 
starting (let's call it log-on-start) or as it's finishing (log-on-finish). For 
an event "read-file," the former might mean a "read-file" is logged as soon as 
some reading function is entered, whereas a log-on-finish system would create 
the log line as when the file reading finished. This has an impact on how 
Perfume invariants and models are interpreted.

For log-on-start, invariant bounds are between the start of event A and the 
start of event B (so they don't include the metric of event B). In addition, 
metrics for one node/event are in its outgoing edges, and the last event in any 
trace will never have a metric. This is because a metric for an event means 
"metric value difference between when the next event starts and when I started."

For log-on-finish, invariant bounds are between the end of event A and the end 
of event B (so they don't include the metric of event A). In addition, metrics 
for one node/event are in its incoming edges, and the first event in any trace 
will never have a metric. This is because a metric for an event means "metric 
value difference between when I finished and when the previous event finished."

Document these important distinctions somewhere.

Original issue reported on code.google.com by tonyohm...@gmail.com on 24 Apr 2014 at 11:00

GoogleCodeExporter commented 9 years ago
Related to this, whether logging-on-start or finish impacts how to correctly 
convert Perfume's (currently) default output of an event-based FSM to a 
state-based FSM. This follows from the above discussion:

For log-on-start, event names should be pushed into their outgoing edges 
because their corresponding metric ranges are there. For log-on-finish, event 
names should be pushed into their incoming edges.

This is particularly important if such a conversion is ever integrated into 
Perfume because an incorrect log origin assumption would lead to a very 
misleading state-based model. Specifically, event names would be placed on 
edges next to metric value ranges that don't actually belong to that event.

Issue #403 describes adding state-based model output and is therefore related to this issue (and especially this comment in particular).

Original comment by tonyohm...@gmail.com on 10 Oct 2014 at 7:33