The soda vending machine SPL come from [Classen 2013]. This SPL presents a configurable soda vending machine that can sell both soda and/or tea and accept US dollar or Euro and may provide free drinks.
The Featude Diagram here above presents all the valid combinations of features (i.e., products) for the soda vending machine SPL. For instance, {v, b, t, cur, usd } corresponds to a machine that sells only tea and accept only dollar.
The feature diagram in TVL format (see TVL) may be downloaded here: svm.tvl
The feature diagram in SPLOT format (see SPLOT may be downloaded here: svm.splot.xml
The Featured Transition System (FTS) presents all the valid behaviours of the soda vending machine product line. Transitions are tagged with feature expressions specifying the products that can execute the transition.
For instance: - f in the figure above indicates that only products that have not the free feature may fire the pay, change, open, take and close transitions. A transition system modelling the behaviour of a given product is obtained by removing the transition whose feature expression is not satisfied by the product.
The FTS in XML may be downloaded here : svm.fts
A usage model is a transition system where transitions have probability values defining their occurrence likelihood. This is equivalent to a Deterministic Time Markov Chain (DTMC) with actions on the transitions. Actions are used here as the link to the FTS.
The usage model of the soda vending machine is presented here above. Since the usage model does not consider features, there may exist paths in the DTMC that are inconsistent for the SPL. For example, one can follow the path pay, change, tea, serveTea, take. This path actually mixes pay machine (feature f not enabled) and free machine (feature f enabled). The combined use of DTMCs and FTS allows us to detect such inconsistencies.
The usage model may also be "incomplete" regarding the FTS since some transitions in the FTS may never be fired in any product. For instance, if there is no running product selling soda, the soda, serveSoda transitions are not present in the DTMC.
The usage model in XML may be downloaded here : svm.usagemodel
Trace selection is done using a DFS algorithm which will select traces starting in state 1 and ending in state 1 and which will have a given minimal and maximal probability to be executed. The algorithm also requires a maximal length for the traces in order to avoid infinite loops (e.g., if where have a loop not passing by state 1 in the TS). The signature of the algorithm is the following : DFS(maxLength, PrMin, PrMax, usageModel) returns Set(Traces).
On the sova vending machine example, an execution of the algorithm will give the following results :
DFS (7 ; 0 ; 0.1 ; usageModel-svm.xml) = {
(pay, change, cancel, return) ;
(free, cancel, return) ;
(pay, change, tea, serveTea, open, take, close);
(pay, change, tea, serveTea, take) ;
(free, tea, serveTea, open, take, close)
}Filtering is done using the FTS. The idea is to execute the traces on the FTS to detect invalid traces (i.e., traces that can not be executed by any valid product of the SPL). Practically, this is done by conjuncting the feature expression of the transitions fired when executing a trace and the feature diagram of the SPL, if the formula is satisfyable, then the trace is valid (because there exists a product that can execute it).
In our example, the set of finite traces generated from step 1 contains two illegal traces: (pay, change, tea, serveTea, take) and (free, tea, serveTea, open, take, close). Those 2 traces (mixing free and not free vending machines) cannot be executed on the FTS and will be rejected in this step.
The FTS' is build by keeping only states visited and transitions fired by the legal traces :
At this step, each valid finite trace t is associated to the set of products prod(t,fts') that can actually execute t with a probability Pr(t). Product priortization may be done by classifying the finite traces according to their probability to be executed, giving t-behaviourally equivalent classes of products for each finite trace t. For instance, for the trace (pay, change, tea, serveTea, open, take, close), the products will have to satisfy the - f and t feature expression and the soda vending machine feature diagram. This gives us a set of 8 products (amongst 32 possible):
{ (v, b, cur, t, eur) ;
(v, b, cur, t, usd) ;
(v, b, cur, t, c, eur) ;
(v, b, cur, t, c, usd) ;
(v, b, cur, t, s, eur) ;
(v, b, cur, t, s, usd) ;
(v, b, cur, t, s, c, eur) ;
(v, b, cur, t, s, c, usd) }All of them executing (pay, change, tea, serveTea, open, take, close) with a probability Pr=0.009 which is the lowest probable behaviour of the soda vending machine.
The following archive contains all the files and tools needed to execute the trace prioritization. Please read the contained README.txt file to get information on how to run the prioritization.