specless.inference.timed_partial_order.TPOInferenceAlgorithm

class specless.inference.timed_partial_order.TPOInferenceAlgorithm(heuristic: str = 'order', decimals: int = 2, threshold: float = 0.5)

Bases: InferenceAlgorithm

The inference algorithm for inferring a TPO from a list of TimedTraces.

Parameters:

InferenceAlgorithm (_type_) – _description_

Methods

format_timed_trace
format_timed_traces
get_event_bounds	Compute min and max time boudn for each event
get_event_pair_bounds	Compute min and max time boudn for each event
get_reachability_order	Compute a Reachability order of a graph
infer	Infer a Timed Partial Order (TPO) from a list of timed traces
infer_time_constraints	Infer Time Bounds on Nodes and Edges given Partial Order.
load_abbadingofile_as_timetraces	Load a abbadingo-style data file Files start from (#dataset, #symbols) following a list of (#neg/pos{0,1} #datalength, data)
load_concat_csvfile_as_timedtraces
load_csvfiles_as_timedtraces
select_next_edge_iterator	Select next_edge_iter function
select_post_processing_func	Select a Post Processing Function

static get_event_bounds(traces: List[List[Tuple[Set[str], float]]], partial_order: Dict[str, List[str]] | None = None) → Dict[str, Tuple[float, float]]

Compute min and max time boudn for each event

static get_event_pair_bounds(traces: List[List[Tuple[Set[str], float]]], partial_order: Dict[str, List[str]] | None = None) → Dict[Tuple[str, str], Tuple[float, float]]

Compute min and max time boudn for each event

static get_reachability_order(graph: DiGraph, init_node: str, forward: bool = True) → List

Compute a Reachability order of a graph

infer(dataset: List[List[Tuple[float, str]]]) → Specification | Exception

Infer a Timed Partial Order (TPO) from a list of timed traces

Implementation in detail:

1. For each symbol, we keep all possible

   • forward constraints,

     ex.) symbol < next_symbol,

   • backward constraints,

     ex.) prev_symbol < symbol.

2. If there is a hard constraint in the order, there should NEVER be a same symbol in forward constraints and backwards constraints. Thus, linear constraints = forward_constraints - backward_constraints.

3. We construct a graph based on the linear constraints.

Parameters:

dataset (Dataset) – Timed Trace Data

Returns:

Timed Partial Order

Return type:

Specification

infer_time_constraints(traces: List[List[Tuple[Set[str], float]]], po: PartialOrder, partial_order: Dict[str, List[str]], debug: bool = False, decimals: int | None = None, threshold: float | None = None) → Tuple

Infer Time Bounds on Nodes and Edges given Partial Order.

Notes

Optimization Problem:

\[ \begin{align}\begin{aligned}min c x\ s.t.\ A x <= b\\variables: tau_ei: Time Variable at Event i values: t_ei: Time at Event i from data T_ei: Times at Event i for all traces, i.e., T_ei = [t_ei, ...]\end{aligned}\end{align} \]

\[min: \sum (u_eij - l_eij) + \sum (u_ei - l_eij)\ s.t.)\ tau_e1 >= max(0, min(T_e1)) => -tau_e1 <= -min)\ tau_e1 <= max(T_e1))\ ...)\ tau_e2 - tau_e1 >= max(0, min(T_e2-T_e1)) => -(tau_e2 - tau_e1) <= -min)\ tau_e2 - tau_e1 <= max(T_e2-T_e1))\ ...\]

Thus,

num_variable = num_event num_constraint = 2*num_event + 2*num_pair

x.shape = (num_variable, 1) or simply vector x c.shape = (1, num_variable) or simply vector c^T A.shape = ((num_constraint) x (num_variable)) b.shape = (num_constraint, 1) or simply vector b

static load_abbadingofile_as_timetraces()

Load a abbadingo-style data file Files start from (#dataset, #symbols) following a list of (#neg/pos{0,1} #datalength, data)

For example, 4 2 1 10 a a a a a b b b b b 1 5 a a a a b 1 2 a b 1 10 a a a a a a a a a b

Raises:

NotImplementedError – _description_

select_next_edge_iterator(lp: Type[TimeConstraintsLP], po: PartialOrder, partial_order: Dict[str, List[str]]) → Callable

Select next_edge_iter function

select_post_processing_func()

Select a Post Processing Function