All basic diagrams for telecommunication example are split into three groups:
Complete demo constitutes with the following 6 sections:
The first three sections contain observation of basic protocols from corresponding group, checking transition consistency within this group and resolving found inconsistencies by means of introducing axioms for proving pairwise non-intersection of preconditions. Some of inconsistencies cannot be resolved by adding axioms because the intersection is actually reachable from some initial state. These are examples of feature interaction which can be resolved only by redeveloping basic protocols.