Software configuration often studies two issues: firstly, how to merge various software components together to create a program with a fixed structure that fits the requirements, and secondly, how to effectively set up the remaining (usually installation specific) configuration options when deploying the program. Nowadays, the user demands a simple and well arranged way to set up these options, possibly through a graphical user interface (GUI). There are various tools designed to assist the user with these tasks. In this paper, a general multi-platform configuration tool Freeconf is introduced. Our technique to simplify a GUI, which has been incorporated into Freeconf, is described. This technique is based on a set of properties that allow splitting the universe of configuration options into several categories with a clear semantics and rules that control the dynamics of options distribution to these categories in response to the user's actions. The rules are currently only implemented in the source code of Freeconf as a proof-of-concept without any formal proof of soundness or completeness. Results from the domain of Rule-Based Constraint Programming have been applied in the paper to develop a formal description of the rules.
While working with a software application, the user usually needs to
adjust a working environment to her needs. Nowadays, almost every
application lets the user to perform some configuration. The
average user often does not understand the background of the program
and expects a nice graphical user interface (GUI) to assist her.
However, there are many applications (especially in the GNU/Linux
environment) that do not have any GUI whatsoever and the only way
how to configure them is through configuration text files. A serious
problem of these files is that their syntax differs greatly, so the user
must learn it first from the documentation. It is also necessary for
the user to deeply understand the meaning of various configuration
options (configuration keys), their dependencies, and their possible
values.
There exist tools that address the above mentioned difficulties. Some
are focused on a given domain (or even at one application, Linux
kernel is popular) like SmartFrog [
Many automatic configuration tools suffer from the overwhelming complexity of the user interface they generate which is a severe problem for the user. One of the possibilities of solving this issue consists in breaking the uniform universe of keys to several categories and providing the categories with an exact semantics. Then, only the keys from a category which is the most interesting to the user at a given moment can be displayed. The solution presented here is based on a set of properties of keys, in other words, on a set of labels that are assigned to every key and determine its membership to a category. In Table 1, there is an example of a set of possible properties for keys categorization. The last property undefined represents a set of keys that do not have their value set and therefor could cause problems in the output of the configuration. In other words, this property allows us to describe a form of inconsistency with the instant state of the configuration.
property mandatory meaningful undefined meaning The key is important to the configured application and must be filled in.
The key has sense in the present settings and its existence is not ruled out by any dependency.
The key finds itself in an invalid state such as that it has no value set or the value is in conflict with dependencies.
Having each key as a feature, this approach resembles feature
modeling [
The distribution of keys into categories does not have to be static, some keys can change their roles during the configuration process in response to an outer activity (a dependency event, user input). A mechanism is needed to control the development of the categories. For this, Freeconf uses rules to control the propagation of properties. The current set of rules in Freeconf has been constructed by hand and tested only empirically; it has not been proved, whether the rules are sound or complete. Techniques of the rule-based constraint programming can provide a proof; however, one must first give a formal description to the rules.
The rest of this paper is divided as follows. In Section 2, a brief introduction to Rule-Based constraint programming is presented. Section 3 describes the structure of Freeconf and a set of properties used in the tool. Section 4 introduces the way Freeconf handles propagation of properties. Finally, Section 5 presents a formalized set of rules, and Section 6 concludes. 2
Rule-Based constraint programming is a special case of a more
general constraint programming studied in [
X = x1; : : : ; xn
D1; : : : ; Dn; so each xi takes its value from the set Di.
Definition A constraint C on X is a pair hCR; Xi where CR is an n-ary relation over the domains Di, i.e., CR D1 : : : Dn; of solutions to the constraint.
Definition A constraint satisfaction problem (CSP) is a triple hC; X; Di where X = x1; : : : ; xn is a finite sequence of variables with respective domains D = D1; : : : ; Dn, and C is a finite set of constraints, each on a sub-sequence of X.
Definition A solution to the CSP hC; X; Di is an element d 2 D1 : : : Dn such that for each constraint C 2 C on a sequence of variables Y it holds d [Y ] 2 C where d [Y ] stands for a projection of d to Y = xi(1); : : : ; xi(l), i.e., d [Y ] = di(1); : : : ; di(l). Sol (hC; X; Di) will denote the set of all solutions to the CSP hC; X; Di.
There exist general algorithms for solving a CSP [
The core concept of Rule-Based programming is a rule. Rules are
condition-action pairs where the condition part is used to determine
whether the rule is applicable and the action part defines the action
to be taken [
A)(hC; X; Di) := hC [ B; X; Di hC; X; Di ifA C; otherwise:
Sol(hB; X; Di):
To help the user to overcome difficulties of software configuration, the project Freeconf has been established. The purpose of this project is to unify the existing configuration process and to assist the user by automatically creating the configuration dialog window similar to one in Fig.1. The configuration process must be smooth from the point-of-view of the user: the dialog must fit nicely into the desktop environment, configuration options must be presented in the logical order, and only what is crucial to fill in should be shown. To better understand how Freeconf addresses these tasks, a short description of its inner structure is presented. The project consists of several components as shown in Fig.2. The most important one is the Freeconf library which contains the entire functionality. The library is shared by graphical client applications (clients), the sole purpose of which is to present a configuration dialog to the user. One can have many different clients, each for one desktop environment. The clients are supposed to be very small (less than a 1000 lines of code), so it should be very simple to create another one. To be able to configure an existing application, the library needs to be provided with an appropriate configuration package. The package is a collection of XML files that semantically describe the configuration file the application understands (native configuration file). It contains a list of all keys, their default values, properties and dependencies, and a rough description of what the resulting dialog should look like. Keys can be organized into configuration sections. The number of keys can vary depending on the configured application. Usually, configuration packages have tens to hundreds of keys, but some configurations utilize up to thousands of keys like in the case of the Linux kernel.
When a package is loaded, the library constructs three tree structures — a template tree for storing key properties, a configuration tree for storing values and handling dependencies, and a GUI tree for dialog modeling. The trees are interconnected, and one can freely traverse from one node of one tree to the matching node of another tree. Leave nodes correspond to keys and their properties, the nonleave nodes represent configuration sections (there is always a rootsection present). When a client needs data for dialog construction, it connects to the library through the client-library interface and obtains various properties for each node. Fig.3 shows the situation. The interface forms a tree which is placed between the GUI tree in the library and the hierarchy of GUI elements (group-boxes, line edits, check-boxes, etc.). The client organizes the GUI elements to another tree that is very closely related to the actual look of the dialog. client tree group-box check-box group-box i n t e r f a c e library GUI tree
Every key type adds additional properties, e.g., a number can have a minimum, a maximum, and a step by which the value increments and decrements. String keys usually have a regular expressions associated with them constraining their value.
While the basic set of properties would generally suffice to construct a dialog, the dialog would look overfilled and confusing to the user. That is why another set of properties was added to Freeconf which would enable splitting keys into different categories. Thus, only keys from a specific category can be shown to the user. The current set of properties which extends those presented in Table 1 is summarized in Table 3.
property static mandatory static active dynamic mandatory dynamic active inconsistent empty meaning If it is true, the key is mandatory and must be always shown.
If it is false, the key is not visible to the client.
This property can only be set from a dependency handler. If it is true, the key is mandatory and must be shown. This property has no meaning when the static mandatory property is set to false.
This property can only be set from a dependency handler. If it is false, the key does not have sense in the current settings. This property has no meaning when the static active property is set to false.
The key does not have neither a value, nor a default value set and is dynamically mandatory and dynamically active.
The property is only applicable to section nodes. It states whether the section is empty, i.e., all its children are hidden.
All static properties are stored in the package as a part of a template describing the native configuration file, while the dynamic ones are a part of a file describing dependencies.
Mandatory property states, whether the key is important or not. Important keys should be visible in the dialog while non-mandatory keys can be hidden, so the dialog becomes less confusing. The static version of this property is used for packages with no dependencies or for keys unaffected by any dependency. The dynamic version can, as in the current version of Freeconf, override the static state only when the static mandatory property is not false (that means static non-mandatory keys are definite).
Active property has two different semantics. In its static version, it is used to prevent the library from announcing the key to the client. In other words, if the property is set to false, the key is virtually commented out. It is easier to disable the key that way than to delete it from the entire package which is non-trivial. The dynamic version of this property serves the purpose of ruling out situations that do not have sense (e.g., when the user checks the "no sound" option, setting the "volume" option becomes nonsensical and this option should be left out from the dialog or at least disabled).
Inconsistency is a special situation when the key does not have any value set, but it is important to the configured program. This can happen, especially when the configuration is run for the first time, and there exist keys which do not have default value set by the creator of the package. When this situation occurs, the user has to be told so and must be able to solve the problem with minimum effort. It follows from the above mentioned description of the properties there are situations where inconsistency is acceptable and the user needs not to be alerted (e.g., when the key is statically inactive). In fact, there exists exactly one combination of the properties which needs some user assistance (i.e., the client must be informed) — the key is dynamically mandatory, dynamically active, and inconsistent at the same time. In other situations, such as when the key is only dynamically active but not mandatory, the key is simply left out from the native output (so the native output will always contain only keys with a defined value).
Emptiness is an important property which naturally arose from the need of hiding non-mandatory keys. The user cannot be distracted by optional keys, so those must be hidden. If there is a section containing only hidden keys, there is no point of displaying it. The empty property can help the client with hiding of unnecessary GUI elements. 4
Freeconf maintains properties in connected tree structures as described in Section 3. The Freeconf library must be able to inform the clients about the state of each property in every node the client– library interface announces. For leave nodes, this becomes trivial. For non-leave nodes, however, the state of a property must reflect what is happening in all of node’s direct successors. 4.1
To keep record of the number of properties in children nodes, every section has a set of counters, each bound to a specific property. Counters hold how many times the matching property occurs in the successors. For example, for the inconsistent property the "inconsistent count" counter exists in each section and if it is, for instance, set to two, then there are exactly two children nodes that are inconsistent.
If a counter reaches zero, a message about the change of a property is sent to the client from the affected section. The section must also inform its parent (i.e., another section) about the change, so the appropriate counter of the parent can be adjusted. Similarly, a message must be sent whenever a nullified counter is incremented.
The entire propagation schema can be seen in Fig.4.
When the state of a property (inconsistency in this case) has been changed, the node notifies its parent about the change. The parent section increments or decrements the matching counter and checks, whether the counter is zero or not. If it is zero, the notification is propagated further up the tree. This leads to the expected behavior in the client since every path leading to an inconsistent key is marked, so the client can render it appropriately. The top-level section (a configuration tab in fact) also knows about the overall state of all keys underneath and it can, for instance, forbid creating the native output until all inconsistencies have been resolved. This method requires a protection mechanism against resending the same message. An obvious solution would be to remember the last state of each property for every node and inform the parent only if the state changes.
For this algorithm to be valid, all counter must be set to the correct value at start time. This is called the initialization phase. All counters are set to zero, and the tree is traversed by depth-first search. Every leave node is evaluated and the existing propagation framework is used to initialize all counter values.
It is also possible to emit a global change, for instance, when the user overrides the mandatory property and enforces showing all keys which are dynamically active. In such a case, all leave nodes are asked to reevaluate their states similarly to the initialization phase. In fact, the initialization phase is a form of a global change. 5
The above mentioned algorithm was implemented in an ad hoc manner. All property evaluation procedures were tailored to the semantics described in Section 3. The result is a set of rules implemented as condition statements in the source code.
The goal of this section is to bring a formal description of the resulting rules based on definitions from Section 2. 5.1
Let K = fk1; : : : ; kng be a set of indices for keys and S = fs1; : : : ; slg a set of indices for sections. Let parent : K [ S ! S [ f;g be a mapping returning for each key or section its parent. The symbol of an empty set is returned for the top-level section. All properties of keys will be modeled as Boolean variables. For example, dynactx will denote a dynamic active property of a key with an index x 2 K. Together with the properties from Table 3, variables def valsetx and valsetx will be used to describe the states where a default value and a value have been set to the key, respectively.
Section counters will be modeled as non-negative integer variables. As an example, inconsistcounty represents the state of an inconsistent counter in a section with an index y 2 S. If the index is ;, no action is performed.
Moreover, there is a Boolean variable called showallact which enables showing even non-mandatory properties (i.e., showing all active keys regardless of the state of the mandatory property). The list of all rules currently used in Freeconf follows.
In the initialization phase, dynactx and dynmanx are set according to the static version of the properties and inconsistentx is evaluated for the first time.
When the valsetx variable changes its value, these rules are applied to update inconsistency.
:inconsistentx :(:def valsetx ^ :valsetx)^ ^ inconsistentx 8x 2 K
Whenever either dynmanx or dynactx variable changes its value, the inconsistent state of the node must be reevaluated and the parent’s counter is adjusted accordingly.
dynactx dynmanx inconsistentx inconsistentx staticactx 8x 2 K staticmanx 8x 2 K (:def valsetx ^ :valsetx)^ ^ dynmanx ^ dynactx 8x 2 K (:def valsetx ^ :valsetx)^ ^ :inconsistentx ^ dynmanx^
dynmanx ^ inconsistentx ^ dynactx 8x 2 K dec(inconsistcountparent(x))
(dynmanx ^ inconsistentx ^ :dynactx)_ _ (dynactx ^ inconsistentx^ ^ (:dynmanx _ :inconsistentx)) 8x 2 K
If the inconsistcounty alters, the section must test if it is not necessary to propagate the information further.
dec(inconsistcountparent(y)) ^ :inconsistenty
(inconsistcounty = 0) ^ inconsistenty 8y 2 S inc(inconsistcountparent(y)) ^ inconsistenty
:(inconsistcounty = 0) ^ :inconsistenty 8y 2 S The mandatoryshowny and activeshowny counters change when a dependency alters dynmanx and dynactx, respectively. It must be also tested whether the static equivalents to the respective properties have not been set to false.
:emptyy ^ dec(sectionshownparent(y))
emptyy ^ :(sectionshowny = 0)_ _ (showallact ^ :(activeshowny = 0))_ _ (:showallact ^ :(activeshowny = 0)^ ^ :(mandatoryshowny = 0)) 8y 2 S emptyy ^ inc(sectionshownparent(y))
:emptyy ^ ((mandatoryshowny = 0)^ ^ (sectionshowny = 0)) _ ((activeshowny = 0)^ ^ (sectionshowny = 0)) 8y 2 S 5.2
It can be easily seen that some of the rules are not optimal. For instance, the second rule in 1 could be shortened by leaving out the last occurrence of inconsistentx. In 2, the rules should be mutually exclusive, but it is non-trivial showing the head formulas really behave that way. (1) (2)
Clearly, a problem of the current implementation is the lack of formal description. All condition statements are scattered across the source code, and it is very complicated maintaining them even though the number of the properties is very small. The design is also not very robust since a small change in any of the conditions will render the system non-functioning. This actually happened — one conjunction was overwritten by mistake by a disjunction, and the client started behaving strangely. It was obvious there was a mistake in a condition, but it was difficult to find it. 6
This paper introduces Freeconf, a multi-platform configuration tool, and a technique which reduces the problem of very complex graphical user interfaces that are often generated by automatic configuration tools. The technique is based on splitting configuration options into categories using properties and forming a set of rules that control the dynamics of the evolution of the categories. A set of rules has been proposed to be used in Freeconf to simpify its graphical output. The rules have been implemented in the source code as a proof-ofconcept, and it has been empirically verified that the rules work. In this paper, a formal description of the rules has been presented based on the theory of Rule-Based programming. The proof of soundness and completeness of the rules is subject of future work. 7
This work was partially supported by the project of the Student Grant Agency of the Czech Technical University in Prague No. SGS11/161/OHK4/3T/14, 2011-13 and Research Direction Project of the Ministry of Education of the Czech Republic No. MSM6840770010. [13] K. Marriott and P.J. Stuckey, Programming With Constraints: An Introduction, Mit Press, 1998. [14] Nico Roos, Yongping Ran, and H. Jaap van den Herik, ‘Combining Local Search and Constraint Propagation to Find a Minimal Change Solution for a Dynamic CSP’, in Proceedings of the 9th International Conference on Artificial Intelligence: Methodology, Systems, and Applications, AIMSA ’00, pp. 272–282, London, UK, UK, (2000). SpringerVerlag. [15] V. Saraswat and P. Van Hentenryck, Principles and Practice of Constraint Programming: The Newport Papers, chapter The SkyBlue Constraint Solver and Its Applications, 385–405, Mit Press, 1995. [16] Sven Vermeulen, ‘Linux sea’. http://swift.siphos.be/linux_sea, 2012.