Irman Faqrizal

Gwen Salaün

Counting Bugs in Behavioural Models using Counterexample Analysis

Keywords: Behavioural Models, Model Checking, Debugging, Counterexample, Bug Counting

Designing and developing distributed software has always been a tedious and error-prone task, and the ever increasing software complexity is making matters even worse. Model checking automatically verifies that a model, e.g., a Labelled Transition System (LTS), obtained from higher-level specification languages satisfies a given temporal property. When the model violates the property, the model checker returns a counterexample, but this counterexample does not precisely identify the source of the bug. In this work, we propose some techniques for simplifying the debugging of these models. These techniques first extract from the whole behavioural model the part which does not satisfy the given property. In that model, we then detect specific states (called faulty states) where a choice is possible between executing a correct behaviour or falling into an erroneous part of the model. By using this model, we propose in this paper some techniques to count the number of bugs in the original specification. The core idea of the approach is to change the specification for some specific actions that may cause the property violation, and compare the model before and after modification to detect whether this potential bug is one real bug or not. Beyond introducing in details the solution, this paper also presents tool support and experiments.

INTRODUCTION

Designing and developing distributed software has always been a tedious and error-prone task, and the ever increasing software complexity is making matters even worse. Model checking [START_REF] Baier | Principles of Model Checking[END_REF] is an established technique for automatically verifying that a model, e.g., a Labelled Transition System (LTS), obtained from higher-level specification languages such as process algebra satisfies a given temporal property, e.g., the absence of deadlocks. When the model violates the property, the model checker returns a counterexample, which is a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the specification is a complicated task for several reasons: (i) the counterexample can contain hundreds (even thousands) of actions, (ii) the debugging task is mostly achieved manually, (iii) the counterexample does not explicitly highlight the source of the bug that is hidden in the model, (iv) the counterexample describes only one occurrence of the bug and does not give a global view of the problem with all its occurrences.

In this work, we rely on some debugging techniques proposed in [START_REF] Barbon | Debugging of Behavioural Models using Counterexample Analysis[END_REF]. These techniques aim at extracting the part of the whole behavioural model which does not satisfy the given property. This model is called a counterexample LTS. In that LTS, some specific states are identified from which the specification can reach a correct part of the model or an incorrect one. These faulty states correspond to decision points or choices that are particularly interesting because they usually point out a part of the model that may identify the source of the bug. Once all the faulty states have been identified, visualization techniques are used to graphically observe the whole model and see how those states are distributed over that model.

One limit of this approach is that it does not give any clue on how much erroneous is the specification and corresponding model. We do not know if there is one bug in the application or several ones. This information is important to quantify the faulty part of the model and thus to measure the effort for debugging the program. Moreover, bugs are usually considered to be all identical in terms of importance. However, this is not the case in practice, and some of them are more critical than others. As an example, a bug can only occur in a very specific situation whereas another one can systematically occur and thus make the whole program erroneous.

In this paper, we propose some techniques to count the number of bugs in a given specification. This approach relies on the idea of modifying the specification and of analyzing the changes in the corresponding model. As a result, we provide as output the number of bugs in the specification with some information regarding the kind of bugs. This information serves to quantify the degree of faultiness of the specification and can be used as a measure to evaluate the effort necessary to correct the specification. In this work, we focus on safety properties, which state that something wrong must not happen. These properties are widely used in the verification of real-world systems. The violation of a safety property occurs when the specification contains certain sequences of actions invalidating the property. We will show in this work how we take advantage of the last actions in these sequences to identify and count the number of bugs.

More precisely, our approach takes as input a specification that can be compiled into an LTS (or directly an LTS) and a safety property written using a temporal logic. In this work, we use LNT [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 6.7)[END_REF] and MCL [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF], respectively, as specification language and temporal logic. We first apply some successive changes to the specification to highlight some actions (known as last actions in the property) that may be the cause of bugs. Then, every time the specification is modified, we generate the corresponding counterexample LTS. By comparing the successive versions of the counterexample LTS, we are able to detect whether each potential bug is really a bug or not. At the end, we can return the number of bugs and for each bug we indicate whether it is inevitable or avoidable. This approach is fully automated by a tool we implemented and applied on several examples for validation purposes.

The rest of this paper is organized as follows. Section 2 introduces some preliminary notions on behavioural models and faulty states. Section 3 presents the details of our approach for bug counting. Section 4 introduces the tool support and some experiments we carried out for validating our approach. Section 5 surveys related work and Section 6 concludes the paper.

BACKGROUND

In this work, we adopt Labelled Transition System (LTS) as behavioural model of concurrent programs. An LTS consists of states and labelled transitions connecting these states. An LTS is produced from a higher-level specification of the system described with a process algebra for instance. Specifications can be compiled into an LTS using specific compilers. In this work, we use LNT as specification language [START_REF] Champelovier | Reference Manual of the LNT to LOTOS Translator (Version 6.7)[END_REF] and compilers from the CADP toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] for obtaining LTSs from LNT specifications. However, the approach presented in this section is generic in the sense that it applies on LTSs produced from any specification language and any compiler/verification tool.

LNT is an extension of LOTOS [START_REF] Iso | LOTOS -A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour[END_REF], an ISO standardized process algebra, which allows the definition of data types, functions, and processes. Table 1 provides an excerpt of the behavioural fragment of LNT syntax. 𝐵 stands for a LNT term, 𝐴 for an action, 𝐸 for a Boolean expression, 𝑥 for a variable, 𝑇 for a type, and 𝑃 for a process name. The syntax fragment presented in this table contains the termination construct (stop) and the occurrence of actions (𝐴) that may come with offers (send an expression 𝐸 or receive in a variable 𝑥). LNT processes are then built using several operators: sequential composition (;), conditional statement (if), non-deterministic choice (select), parallel composition (par) where the communication between the involved processes is carried out by rendezvous on a list of synchronized actions, looping behaviours described using process calls or explicit operators (while), and assignment (:=) where the variable should be defined beforehand (var). LNT is formally defined using operational semantics based on LTSs. An LTS can be viewed as all possible executions of a system. One specific execution is called a trace. Definition 2.2. (Trace) Given an LTS 𝑀 = (𝑆, 𝑠 0 , Σ,𝑇 ), a trace of size 𝑛 ∈ N is a sequence of labels 𝑙 1 , 𝑙 2 , . . . , 𝑙 𝑛 ∈ Σ such that

𝐵 ::= stop | 𝐴 (!𝐸, ?𝑥) | 𝐵 1 ; 𝐵 2 | if 𝐸 then 𝐵 1 else 𝐵 2 end if | select 𝐵 1 []...[]𝐵 𝑛 end select | par 𝐴 1 , ...,
𝑠 0 𝑙 1 -→ 𝑠 1 ∈ 𝑇 , 𝑠 1 𝑙 2 -→ 𝑠 2 ∈ 𝑇 , . . . , 𝑠 𝑛-1 𝑙 𝑛 --→ 𝑠 𝑛 ∈ 𝑇 .
The set of all traces of 𝑀 is written as 𝑡 (𝑀).

Model checking consists in verifying that an LTS model satisfies a given temporal property 𝑃, which specifies some expected requirement of the system. Temporal properties are usually divided into two main families: safety and liveness properties [START_REF] Baier | Principles of Model Checking[END_REF]. In this work, we focus on safety properties, which are widely used in the verification of real-world systems. Safety properties state that "something bad never happens". A safety property is usually formalized using a temporal logic. We use MCL (Model Checking Language) [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF] in this work, which is an action-based, branching-time temporal logic suitable for expressing properties of concurrent systems. MCL is an extension of alternation-free 𝜇-calculus with regular expressions, data-based constructs, and fairness operators. A safety property can be semantically characterized by an infinite set of traces 𝑡 𝑃 , corresponding to the traces that violate the property 𝑃 in an LTS. If the LTS model does not satisfy the property, the model checker returns a counterexample, which is one of the traces characterized by 𝑡 𝑃 . Definition 2.3. (Counterexample) Given an LTS 𝑀 = (𝑆, 𝑠 0 , Σ,𝑇 ) and a property 𝑃, a counterexample is any trace which belongs to 𝑡 (𝑀) ∩ 𝑡 𝑃 .

The new contributions of this paper rely on existing results presented in [START_REF] Barbon | Debugging of Behavioural Models using Counterexample Analysis[END_REF]. This approach takes as input a specification and a temporal property, and identifies decision points where the specification (and the corresponding LTS model) goes from a (potentially) correct behaviour to an incorrect one. These choices turn out to be very useful to understand the source of the bug. These decision points are called faulty states in the LTS model.

In order to detect these faulty states, the transitions in the model first need to be categorized into different types. The type of a transition indicates whether that transition belongs to traces satisfying the property or not. More precisely, transitions in the LTS can be categorized into three types:

• A correct transition belongs to traces of the LTS for which the property is satisfied. • An incorrect transition belongs to traces of the LTS for which the property is violated.

• A neutral transition is a transition where the validity of the property is not yet determined. The information concerning the transition type (correct, incorrect and neutral transitions) is added to the LTS in the form of tags. The set of transition tags is defined as Γ = {𝑐𝑜𝑟𝑟𝑒𝑐𝑡, 𝑖𝑛𝑐𝑜𝑟𝑟𝑒𝑐𝑡, 𝑛𝑒𝑢𝑡𝑟𝑎𝑙 }. Given an LTS 𝑀 = (𝑆, 𝑠 0 , Σ,𝑇 ), a tagged transition is represented as 𝑠 (𝑙,𝛾 ) ----→ 𝑠 ′ , where 𝑠, 𝑠 ′ ∈ 𝑆, 𝑙 ∈ Σ and 𝛾 ∈ Γ. Thus, an LTS in which each transition has been tagged with a type is called tagged LTS.

𝑇 𝑇 ⊆ 𝑆 𝑇 × Σ 𝑇 × Γ × 𝑆 𝑇 .
It is worth noting that a specific action appearing just once in the LNT specification can appear several times in the corresponding tagged LTS possibly with a different type. This is the case for instance when we have a choice between A and B, both followed by C (select A [] B end select ; C in LNT), and the property states that we do not want A and C in sequence. In that case, the sequence A followed by C corresponds to two incorrect transitions in the tagged LTS whereas the sequence B followed by C corresponds to two correct transitions.

The tagged LTS where transitions have been typed allows us to identify faulty states in which an incoming neutral transition is followed by a choice between at least two transitions with different types (correct, incorrect, neutral). Such a faulty state consists of all the neutral incoming transitions and all the outgoing transitions. -----→ 𝑠 1 ∈ 𝑇 𝑇 and

∃𝑡 2 = 𝑠 (𝑙 2 ,𝛾 2 )
-----→ 𝑠 2 ∈ 𝑇 𝑇 where 𝑡 1 and 𝑡 2 are neutral, correct or incorrect transition, with different tags (𝛾 1 ≠ 𝛾 2 ). In that case, the faulty state 𝑠 consists of the set of transitions 𝑇 nb ⊆ 𝑇 𝑇 such that for

each 𝑡 ′ ∈ 𝑇 nb , either 𝑡 ′ = 𝑠 ′ (𝑙,𝛾 ) ----→ 𝑠 ∈ 𝑇 𝑇 or 𝑡 ′ = 𝑠 (𝑙,𝛾 ) ----→ 𝑠 ′′ ∈ 𝑇 𝑇 .
By looking at outgoing transitions of a faulty state, four kinds of faulty states can be identified (Figure 1 (c)): (1) with at least one correct transition and one neutral transition (no incorrect transition), (2) with at least one incorrect transition and one neutral transition (no correct transition), (3) with at least one correct and one incorrect transition (no neutral transition), and (4) with at least one correct, one incorrect, and one neutral transition. Finally, the notion of counterexample LTS is defined and will be used in the rest of this paper. Definition 2.6. (Counterexample LTS) Given a tagged LTS 𝑀 𝑇 = (𝑆 𝑇 , 𝑠 0 𝑇 , Σ 𝑇 ,𝑇 𝑇 ) and the set of faulty states 𝐹 computed on this tagged LTS, the corresponding counterexample LTS is the tuple 𝐶 = (𝑀 𝑇 , 𝐹 ).

The reader interested in more details regarding the algorithms for computing tagged and counterexample LTSs can refer to [START_REF] Barbon | Debugging of Behavioural Models using Counterexample Analysis[END_REF]. Counterexample LTSs can be visualized to give to the developer a graphical representation of these LTS models where correct/incorrect/neutral transitions and faulty states are highlighted. These visualization techniques make use of different styles and colours to distinguish the different types of transitions and states, as defined in Figure 1. There are three types of transitions (Figure 1 (a)): neutral transitions are represented using (black) dotted lines, correct transitions are represented using (green) solid lines, and incorrect transitions are represented using (red) dashed lines. As for states (Figure 1 (b)), white is used for regular states, (red) solid color with -2 as the state's identifier is used for incorrect sink states, and (green) solid color with -1 as the state's identifier is used for correct sink states. When a state is green or red, this is a sink state because from here the remaining states will be of the same color, so it is not necessary to keep that part of the LTS. Faulty states are represented with different shades of yellow depending on the type of the outgoing transitions (as shown in Figure 1 (c)).

Example. An example of LNT specification is presented in Listing 1. Suppose the property to be respected by this specification states that B should not be executed before A. This is formalized in MCL as follows: By looking at the specification, we can see that the property can be violated in several ways. For instance, in the parallel statement at line 10, there is a possibility to execute B followed by EXEC2 then A, or EXEC2 followed by B then A. Both sequences violate the property because B is executed before A.

[ (𝑛𝑜𝑡 𝐴) * . 𝐵 ] 𝑓 𝑎𝑙𝑠𝑒 (1)
The counterexample LTS generated from this specification and property is given in Figure 2. The counterexample LTS is an LTS composed of all possible counterexamples. For instance, in the case of the property's violation at line 10, one of the corresponding counterexamples is: INIT1 (from state 0), EXEC1 (from state 1), INIT2 (from state 2), EXEC2 (from state 3), B (from state 4). This counterexample LTS exhibits all types of faulty states. As an example, the faulty state identified by 3 is a faulty state with neutral, correct, and incorrect transitions. From this state, the property's violation can be temporarily avoided by executing EXEC2 (neutral transition), can be definitely avoided by executing EXEC3 (correct transition), or can be violated by executing B (incorrect transition). Some states and transitions are hidden in the counterexample LTS because they are replaced by the (correct or incorrect) sink states. For example, in state 1 by executing B, the transition goes to an incorrect sink state (state -2). In that case, since the property becomes false, it is not useful to show any of the following states and transitions.

COUNTING BUGS

Given a specification (written in LNT) and a temporal property (written in MCL), we propose a method for counting the number of bugs. These techniques rely on several notions we will successively present in this section. First, we define the notion of last actions in property, which are the actions executed just before the property becomes false. We also define two different types of bugs called inevitable and avoidable bugs. When a bug is detected, the solution presented in this section is also able to indicate whether the bug is inevitable or avoidable. The techniques for counting bugs rely on the notion of dummy choice, which aims at replacing in the specification an occurrence of a last action in property by a choice between this action and a dummy action. This dummy choice is crucial to identify whether this action corresponds to a part of the specification where the property is violated or not. By relying on this notion of dummy choice, we present an algorithm, which computes the number of bugs and indicates for each bug whether it is inevitable or avoidable. This section ends with the generation of more precise counterexamples, by taking advantage of the information computed when counting the number of bugs.

Last Actions in Property

In this paper, we focus on safety properties. The main idea is that the last actions in the property are the actions executed just before the property becomes false. Therefore, these actions play a central role in the computation of the truth value of the property. In this work, these properties are written in MCL and have the following form: [ 𝑅 ] 𝑓 𝑎𝑙𝑠𝑒, where 𝑅 is a regular expression. The syntax of regular expressions is given by:

𝑅 ::= 𝑡𝑟𝑢𝑒 | 𝑎 | ¬𝑎 | 𝑎 1 ∨ 𝑎 2 | 𝑅1.𝑅2 | 𝑅1|𝑅2 | 𝑅1 *
where 𝑎 ∈ Σ for a given LTS 𝑀 = (𝑆, 𝑠 0 , Σ,𝑇 ). We assume that the regular expression is not empty, therefore the set of last actions in property is not empty either and is computed by a function called 𝑙𝑎𝑠𝑡. Note that ∨ and | are slightly different because ∨ applies on actions whereas | applies on formulas. There is no ∧ operator in the syntax because this predicate results in a property that always evaluates to true1 . Definition 3.1. (Last Actions in Property) Given a safety property [ 𝑅 ] 𝑓 𝑎𝑙𝑠𝑒, function 𝑙𝑎𝑠𝑡 takes 𝑅 and Σ as inputs and returns the set of last actions in this property. Function 𝑙𝑎𝑠𝑡 is defined as follows:

𝑙𝑎𝑠𝑡 (𝑡𝑟𝑢𝑒, Σ) = Σ 𝑙𝑎𝑠𝑡 (𝑎, Σ) = {𝑎} 𝑙𝑎𝑠𝑡 (¬𝑎, Σ) = Σ \{𝑎} 𝑙𝑎𝑠𝑡 ( 𝑎 1 ∨ 𝑎 2 , Σ) = {𝑎 1 , 𝑎 2 } 𝑙𝑎𝑠𝑡 (𝑅1.𝑅2, Σ) = 𝑖 𝑓 𝑒𝑚𝑝𝑡𝑦 (𝑅2) 𝑡ℎ𝑒𝑛 𝑙𝑎𝑠𝑡 (𝑅1, Σ) 𝑒𝑙𝑠𝑒 𝑙𝑎𝑠𝑡 (𝑅2, Σ) 𝑒𝑛𝑑 𝑖 𝑓 𝑙𝑎𝑠𝑡 (𝑅1|𝑅2, Σ) = 𝑙𝑎𝑠𝑡 (𝑅1, Σ) ∪ 𝑙𝑎𝑠𝑡 (𝑅2, Σ) 𝑙𝑎𝑠𝑡 (𝑅1 * , Σ) = ∅
where function 𝑒𝑚𝑝𝑡𝑦 takes as input a regular expression and returns 𝑡𝑟𝑢𝑒 if this expression is the empty word and 𝑓 𝑎𝑙𝑠𝑒 otherwise.

Example. We illustrate the computation of last actions in a property with several properties. First, consider the following property, stating that action CLOSE should not be executed after action EXEC. This property is written in MCL as follows:

[𝑡𝑟𝑢𝑒 * . 𝐸𝑋 𝐸𝐶 . 𝑡𝑟𝑢𝑒 * . 𝐶𝐿𝑂𝑆𝐸] 𝑓 𝑎𝑙𝑠𝑒 (2)
In this property, action CLOSE is the last action in property because it is the only action which is executed just before the property becomes false. Consider now a property stating that when EXEC is executed then CLOSE must not be executed right after it:

[𝑡𝑟𝑢𝑒 * . 𝐸𝑋 𝐸𝐶 . ¬ 𝐶𝐿𝑂𝑆𝐸] 𝑓 𝑎𝑙𝑠𝑒 (3)
In this case, the last actions in property is the set of all actions in the alphabet of the LTS model except CLOSE, that is, Σ \{𝐶𝐿𝑂𝑆𝐸}. This example shows that the last action in property is not always the rightmost action written in the property. Let us assume finally that we do not want the execution of a sequence of OPEN or CLOSE actions, which is written in MCL as follows:

[𝑡𝑟𝑢𝑒 * . (𝑂𝑃𝐸𝑁 . 𝑂𝑃𝐸𝑁 ) | 𝑡𝑟𝑢𝑒 * . (𝐶𝐿𝑂𝑆𝐸 . 𝐶𝐿𝑂𝑆𝐸)] 𝑓 𝑎𝑙𝑠𝑒 (4)
The resulting set of last actions consists of two actions { OPEN, CLOSE }. In the rest of this paper, we will assume that the property has a unique last action for simplifying the presentation, but a property can have several last actions as illustrated previously.

Inevitable and Avoidable Bugs

A bug is called an inevitable bug when the property's violation can not be avoided from the initial state of the LTS model. In that case, there is no trace in the model satisfying the property. In contrast, an avoidable bug is a bug where the violation of the property can be avoided. This means that there exists at least a trace in the LTS model for which the property is not violated. Example. We illustrate this with the LNT specifications given in Listings 2 and 3. The property we want to verify on these specifications was introduced in Section 3.1 and states that action CLOSE should not be executed after action EXEC. In Listing 2, there is an inevitable bug because CLOSE (line 10) is always executed after EXEC (line 4). In Listing 3, there is a possibility to execute CLOSE (line 9) after EXEC (line 4) is executed. However, it is also possible to execute the first part of the select statement (line 6) and thus avoid the property violation. This means that the bug is avoidable. The counterexample LTS corresponding to the LNT specification given in Listing 2 is shown in Figure 3 (a). It has all incorrect (red) transitions because the property violation is inevitable from the initial state. In contrast, the counterexample LTS for Listing 3 (Figure 3 (b)) exhibits one faulty state (state 2): if AA is executed, the bug is avoided, whereas if CC is executed, the property is violated. Note that in this second counterexample LTS, all states and transitions after AA are hidden and replaced by a correct sink state (i.e., BB is missing) because it is not possible to violate the property after AA is executed.

Dummy Choices

The techniques for counting bugs rely on the notion of dummy choice. Given an action, the main idea is to replace the occurrence of this action by a choice in the specification between executing this action and executing a fresh action called dummy action. For debugging purposes, the action replaced by a dummy choice corresponds to the last action in property. Indeed, the property violation occurs when the last action in property is executed. Our method aims at adding a new choice in the specification in order to avoid this execution. This dummy choice helps to identify whether this specific occurrence of the last action may cause the violation of the property (real bug) or not. To do so, we need two versions of the specification: a version where the dummy choice has been added and the version where that dummy choice has been removed. For each version of the LNT specification, we generate the corresponding counterexample LTS. As a result, we have two counterexample LTSs and we compare them in order to decide whether this occurrence of the last action in property corresponds to a real bug or not. More precisely, this comparison has three possible outcomes:

(1) Transition(s) labelled with dummy action(s) are missing from non-faulty state(s) in the second counterexample LTS. In this case, the occurrence of the last action in property does not correspond to a bug. (2) At least one transition labelled with a dummy action is missing from a faulty state in the second counterexample LTS. This means that the occurrence of the last action in property corresponds to an avoidable bug.

(3) The counterexample LTS changed to a counterexample LTS with all incorrect transitions. This means that the occurrence of the last action in property corresponds to an inevitable bug. These three cases are written more formally in the following definition. 𝑇 ,𝑇 ′ 𝑇 ), 𝐹 ′ ) generated from two specifications 𝐿 (with a dummy choice) and 𝐿 ′ (without that dummy choice), the three possible outcomes obtained by comparing 𝐶 and 𝐶 ′ are as follows:

(1) No bug: ∀𝑡 = 𝑠

(𝐷𝑈 𝑀𝑀𝑌 ,𝛾 ) -----------→ 𝑠 ′ ∈ 𝑇 , 𝑠 ∉ 𝐹, 𝑎𝑛𝑑 𝑡 ∉ 𝑇 ′ (2) Avoidable bug: ∃𝑡 = 𝑠 (𝐷𝑈 𝑀𝑀𝑌 ,𝛾 ) -----------→ 𝑠 ′ ∈ 𝑇 , 𝑠 ∈ 𝐹, 𝑎𝑛𝑑 𝑡 ∉ 𝑇 ′ (3) Inevitable bug: ∃𝑠 (𝐴,𝑐𝑜𝑟𝑟𝑒𝑐𝑡 ) ----------→ 𝑠 ′ ∈ 𝑇 , 𝑎𝑛𝑑 ∀𝑠 ′′ (𝐴 ′ ,𝛾 ′ ) ------→ 𝑠 ′′′ ∈ 𝑇 ′ , 𝛾 ′ = 𝑖𝑛𝑐𝑜𝑟𝑟𝑒𝑐𝑡
Note that these three cases are exclusive and cover all possible cases. By removing a dummy choice, the counterexample LTS entirely change (case (3), this is an inevitable bug) or not. If this is not an inevitable bug, there are only two cases: (i) removing the dummy choice has no real impact in the sense that there is just one less transition (case (1)), or (ii) removing the dummy choice has an impact, which results in the presence of a new faulty state in the corresponding counterexample LTS.

Example. Consider the LNT specifications given in Listings 2 and 3. The last action in property consists of the action CLOSE. Therefore, for both examples, our technique replaces the actions CLOSE at line 10 in Listing 2 and line 9 in Listing 3 by the following select statement:

𝑠𝑒𝑙𝑒𝑐𝑡 𝐶𝐿𝑂𝑆𝐸 [] 𝐷𝑈 𝑀𝑀𝑌 𝑒𝑛𝑑 𝑠𝑒𝑙𝑒𝑐𝑡

The corresponding counterexample LTSs are given in Figure 4 (a) and (b). In the first counterexample LTS (Figure 4 (a)), there is a faulty state that has an outgoing transition with a dummy action. If this dummy choice is removed and the counterexample LTS generated, the resulting counterexample LTS consists of incorrect transitions only (Figure 3 (a)). As a result, we can conclude that this occurrence of last action in property corresponds to an inevitable bug (case 3). In the second counterexample LTS (Figure 4 (b)), if the dummy choice is removed in the specification, a dummy action is missing from a faulty state in the generated counterexample LTS (Figure 3 (b)). This means that the corresponding bug is classified as an avoidable bug (case 2).

Algorithm

Before presenting the algorithm computing the number of bugs, we would like to clarify what we mean by one bug and how we count them. Indeed, when the specification does not satisfy a given property, there might be several ways to correct the bug(s) in the corresponding specification. One solution, which induces minimum changes, is to correct the last action in property. In this work, we assume that one bug can be fixed by making a correction where the last action in property is located in the specification, by removing this action for instance. Therefore, the number of bugs in our approach coincides with the number of times one needs to correct the occurrences of the last action in property corresponding to real bugs. We now present Algorithm 1, which takes as input an LNT specification and an MCL property, and returns the number of inevitable and avoidable bugs. The main idea of this algorithm is that we first replace all occurrences of the last action in property by dummy choices. In the next step, by removing the dummy choices one by one and comparing the resulting counterexample LTSs (before and after removal of each dummy choice), we can deduce whether this specific occurrence of last action corresponds to a bug, and if this is the case to which kind of bug.

More precisely, in step 1, the algorithm adds the dummy choices to all occurrences of the last action in property (lines 7 to 13). The corresponding counterexample LTS is then generated (line 14). In step 2, the algorithm loops over all the states in the counterexample LTS. When it finds a dummy action belonging to a transition outgoing from a faulty state, then that dummy action is added to the set of dummy actions 𝐷 ′ (lines 17 to 20). This second step is useful to find all occurrences of the last action in property which correspond to real bugs (case 2 and 3 in Section 3.3).

In the last step, the algorithm loops over the set of remaining dummy actions (line 24). In each iteration, a dummy choice (corresponding to a dummy action in the set) is removed from a copy of the LNT specification, then the counterexample LTS is generated from it (lines 25 to 27). If the counterexample does not have any faulty state, then the number of inevitable bugs is incremented. Otherwise, the number of avoidable bugs is incremented (lines 28 to 31).

As far as the complexity of the algorithm is concerned, the most costly step is to generate counterexample LTSs, which is computed a first time (line 14) and then 𝑛 times where 𝑛 is the number of dummy actions in the set of dummy actions 𝐷 ′ . The counterexample LTS is obtained by first compiling the LNT specification to LTS, and then by computing a product between this LTS and the LTS obtained from the MCL formula. The compilation of LNT to LTS relies on a transformation to Petri nets, whose complexity (exponential) is the same as computing the corresponding marking graph [START_REF] Esparza | Decidability and Complexity of Petri Net Problems -An Introduction[END_REF]. In practice, it is less expensive as parts of the net are 1-bounded. As for the product, the complexity is 𝑂 (𝑆 * 𝑆 𝐹 ) where 𝑆 is the number of states of the initial LTS and 𝑆 𝐹 is the number of states of the formula LTS. As a result, the overall complexity resides in the repetition 𝑛 +1 times of the execution of an exponential algorithm for computing a counterexample LTS.

Last but not least, to go further and actually debug the original specification, we rely on the inevitable bugs to compute what we call the final counterexample LTS. In this LTS, we remove dummy choices for actions that are not bugs or avoidable bugs, but we keep dummy choices for inevitable bugs. This allows us to generate a counterexample with faulty states for all bugs (inevitable and avoidable). We will detail in Section 3.5 how we can take advantage of this final counterexample LTS to compute more precise counterexamples for debugging purposes. Example. Listing 4 gives an example of LNT specification on which we want to check the property introduced beforehand: CLOSE must not be executed after EXEC. There are three bugs in this example. The first one occurs if we execute the first part of the select statement (line 4). The second one occurs when we execute the third part of the select statement (lines 8 to 12). The last one is an inevitable bug and appears at the end of the specification (line 14). The first step of the algorithm is to add dummy choices to all occurrences of the last action in property in the LNT specification. Note that since we increment the dummy action suffix for each addition of a dummy choice, each new dummy action is unique (e.g., in Listing 4, the dummy action in the first dummy select at line 4 is DUMMY1, it is DUMMY2 at line 6, etc.). Figure 5 (a) shows the counterexample LTS generated from the original specification. In that counterexample LTS, all transitions are incorrect because there is one inevitable bug. Figure 5 (b) shows the counterexample LTS corresponding to the specification where each occurrence of the last action in property has been replaced with a dummy choice.

In the next step of Algorithm 1, the counterexample LTS is traversed (Figure 5 (b)) to check if there is any dummy action belonging to transitions outgoing from faulty states. There are three faulty states (states 6, 8, and 10), and each of them has an outgoing transition with a dummy action. Therefore, these dummy actions correspond to real bugs and we add them to the set of dummy actions ({𝐷𝑈 𝑀𝑀𝑌 1, 𝐷𝑈 𝑀𝑀𝑌 3, 𝐷𝑈 𝑀𝑀𝑌 4}).

The last step loops over the set of dummy actions. In each iteration, we remove a dummy choice (from the LNT specification) corresponding to a dummy action in the set, and generate the counterexample LTS. Figure 6 shows the corresponding counterexample LTSs. The counterexample LTS (a) and (b) are the counterexample LTSs generated after the first and second iterations (i.e., removal of the DUMMY1 and DUMMY3 actions). In these two iterations, both generated counterexample LTSs still have faulty states. This implies that these occurrences of the last action in property correspond to avoidable bugs. As for the last iteration, the resulting counterexample LTS (c) is entirely incorrect and thus has no faulty states. This means that this particular occurrence of the last action in property corresponds to an inevitable bug. The algorithm finally returns that this LNT specification exhibits two avoidable bugs and one inevitable bug.

Counterexamples

In this final part of the section, we show how we can generate counterexamples from a counterexample LTS. This makes particulary sense from the final counterexample LTS introduced in Section 3.4. Counterexamples are a classic and simple way to represent a single execution leading to a state where the property is violated. Here, we generate more precise counterexamples because these traces also contain colored transitions and faulty states. Since a counterexample LTS is composed of all possible counterexamples, there are several options for generating counterexamples from such models. Therefore, we propose a set of eleven strategies for generating these counterexamples categorized in four groups: (i) classic counterexamples (e.g., random or shortest counterexample), (ii) counterexamples based on faulty states (e.g., shortest path to a faulty state then shortest counterexample or counterexample with the fewest number of faulty states), (iii) probability-based counterexamples (e.g., the counterexample with the highest probability 2 ), (iv) counterexamples based on the distance to the bug (e.g., the counterexample including the faulty state closest to the incorrect sink state, possibly with the fewest number of faulty states).

For the sake of space, we cannot precisely present all these strategies, but we will present some of them on concrete examples in the rest of this section. The reader can find more details for each strategy in [START_REF] Faqrizal | Debugging and Quantifying Behavioural Models Using Counterexample Analysis[END_REF] as well as guidelines explaining how to choose which strategy to use. It is worth emphasizing that the counterexamples generated here are not classic traces but they also include colors for transitions and (faulty) states as well as all outgoing transitions for faulty states. This information is particularly helpful for debugging purposes.

Example. Consider the counterexample LTS presented in Figure 7, which is the final counterexample LTS after application of Algorithm 1 on the LNT specification given in Listing 4. This is the final counterexample LTS where a single dummy action (DUMMY4) corresponding to the inevitable bug is preserved in this model.

Figure 8 shows a first example of counterexample generated using a classic strategy (shortest counterexample). These counterexamples are usually convenient because they exhibit the shortest trace causing the property's violation. In this case, the sequence of actions is INIT, EXEC, CLOSE. We can deduce from the generated 2 We assume by default that all transitions have equiprobable probabilities. shows another example of counterexample, which was computed in that case using a strategy based on the distance to the bug, namely, the shortest counterexample with a faulty state closest to the incorrect sink state. This counterexample exhibits more faulty states than the former one. The first faulty state shows that CLOSE is the only option to avoid the bug. The second faulty state includes a dummy action, showing that this bug is inevitable, and the execution of action CLOSE leads to the property's violation.

TOOL SUPPORT

In this section, we present the tool support and some experiments we carried out for validating our approach.

Implementation

We have developed a tool in Java which implements the techniques presented in this paper to count the number of bugs. This tool relies on the CLEAR tool [START_REF] Barbon | Debugging of Behavioural Models with CLEAR[END_REF] for computing counterexample LTSs. Figure 9 gives an overview of the tool support. First of all, the last actions in property are computed, followed by the addition of dummy choices to the LNT specification. The tool then locates in the corresponding counterexample LTS the dummy actions which correspond to the property violation. For each dummy action, it identifies the type of bugs (i.e., inevitable or avoidable) by comparing the counterexample LTSs before and after removal of that specific dummy choice. As a result, the tool returns the number of inevitable and avoidable bugs. Finally, the user can generate some specific counterexamples using one of the proposed strategies.

Experiments

In this section, we present some of the experiments we carried out for validating our approach. The goal of these experiments was to evaluate: (i) the accuracy of the results computed by our debugging techniques and (ii) the time it takes to compute these results. Table 2 summarizes some of these experiments on ten realistic case studies. The first three columns characterize the example by giving a name, the reference (when available), the number of lines in LNT, and the size of the corresponding LTS generated from the LNT specification using CADP compilers (S, T, and L, stand for the number of states, transitions, and labels, respectively). As far as outputs are concerned, the three following columns give the size of the final counterexample LTS (S, T, L, and the number of faulty states, FS), the number of inevitable and avoidable bugs, and the time it takes (in seconds) to apply all the steps of our algorithm to compute the expected result.

These experiments allowed us to check whether our results were accurate in terms of number of bugs. To evaluate this goal, we first identify the actual number of inevitable and avoidable bugs by analysis of the program by an independent expert (using classic model checking combined with manual inspection). Then, we compare this result with the output of the tool support (fifth column in Table 2). As a result, both results coincided for all the examples on which these experiments were carried out.

Regarding performance, the objective was to show that it is possible to compute the number of bugs within a reasonable time. Consider for instance the example that takes the longest time to complete in the table, which is the Consumer-Producer example with 10 bugs (fourth row). It requires about three minutes to compute the result. This time mainly comes from the successive generation of the counterexample LTS (for each occurrence of last action in property), which requires the enumeration of all possible execution paths in the input specification. This time increases with the size of the LTS model and with the number of last action occurrences. It is worth mentioning that we do not aim in this paper at solving the state space explosion problem existing for model checking techniques. If we focus on a smaller example (trains stations, last row), it takes less than 30 seconds to compute the result because the LTS is smaller and there are fewer potential bugs in the original specification. Since the verification techniques proposed in this paper are applied at design time, these analysis times are not short but remain reasonable.

RELATED WORK

There are several works which focus on counterexample interpretation and comprehension, see, e.g. [START_REF] Ball | From Symptom to Cause: Localizing Errors in Counterexample Traces[END_REF][START_REF] Tabaei Befrouei | Abstraction and Mining of Traces to Explain Concurrency Bugs[END_REF][START_REF] Groce | What Went Wrong: Explaining Counterexamples[END_REF][START_REF] Jin | Fate and Free Will in Error Traces[END_REF][START_REF] Leue | Mining Sequential Patterns to Explain Concurrent Counterexamples[END_REF][START_REF] Ravi | Minimal Assignments for Bounded Model Checking[END_REF]. In [START_REF] Tabaei Befrouei | Abstraction and Mining of Traces to Explain Concurrency Bugs[END_REF], sequential pattern mining is applied to execution traces for revealing unforeseen interleavings that may be a source of error, through the adoption of the well-known mining algorithm CloSpan [START_REF] Yan | CloSpan: Mining Closed Sequential Patterns in Large Datasets[END_REF]. CloSpan is also adopted in [START_REF] Leue | Mining Sequential Patterns to Explain Concurrent Counterexamples[END_REF], where the authors apply sequential pattern mining to traces of counterexamples to reveal unforeseen interleavings that may be a source of error. However, reasoning on traces as achieved in [START_REF] Tabaei Befrouei | Abstraction and Mining of Traces to Explain Concurrency Bugs[END_REF][START_REF] Leue | Mining Sequential Patterns to Explain Concurrent Counterexamples[END_REF] induces several issues. The handling of looping behaviours is non-trivial and may result in the generation of infinite traces or of an infinite number of traces. Coverage is another problem, since a high number of traces does not guarantee to produce all the relevant behaviours for analysis purposes. As a result, we decided to work on the debugging of LTS models, which represent in a finite way all possible behaviours of the system.

In [START_REF] Jin | Fate and Free Will in Error Traces[END_REF], the authors propose a method to interpret counterexamples generated for liveness properties by dividing them into fated and free segments. Fated segments represent inevitability w.r.t. the failure, pointing out progress towards the bug, while free segments highlight the possibility to avoid the bug. The proposed approach classifies states in a state-based model in different layers (which represent distances from the bug) and produces a counterexample annotated with segments by exploring the model. Our method focuses on locating branching behaviours that affect the property satisfaction whereas their approach produces an enhanced counterexample where inevitable events (w.r.t. the bug) are highlighted. Moreover our approach has a specific focus on safety properties, while they focus on liveness properties.

In [START_REF] Groce | What Went Wrong: Explaining Counterexamples[END_REF], the authors propose automated methods for the analysis of variations of a counterexample, in order to identify portions of the source code crucial to distinguishing failing and successful runs. These variations can be distinguished between executions that produce an error (negatives) and executions that do not produce it (positives). By relying on a notion of control location, their method tries to make sure that such variations are for one bug to avoid multi-bug confusions. The authors then propose various methods to extract common features and differences between the two sets in order to provide feedbacks to the user. Similarly to our work, the work in [START_REF] Groce | What Went Wrong: Explaining Counterexamples[END_REF] also wants to explain the counterexample with a focus on safety properties. In our work, we focus on a model containing all counterexamples, and we take advantage of that model to count the number of bugs. In contrast, their method relies on the analysis of a single counterexample and its variations, making sure that negative variations are from the same bug.

Delta debugging [START_REF] Zeller | Why Programs Fail -A Guide to Systematic Debugging[END_REF] is a well-known line of work on fault localization using testing techniques. The aim of delta debugging consists in understanding the minimal differences (deltas) between a successful and a failing program execution. There have been numerous published papers which rely on delta debugging, but, to the best of our knowledge, none of them allows the bug counting.

Several works aim at providing multiple counterexamples for facilitating debugging. Copty et al. [START_REF] Copty | Efficient debugging in a formal verification environment[END_REF] propose a counterexample wizard to help users when debugging applications using counterexamples. This wizard can retrieve multiple counterexamples, which can be used to understand and fix all reported errors for the given specification. In [START_REF] Busard | Producing Explanations for Rich Logics[END_REF], the authors present a 𝜇-calculus model checker that produces complete and complex counterexamples for branching logics like Computation Tree Logic. This framework also supports additional functionalities to translate these rich explanations back to the original logic. In [START_REF] Dominguez | Generating Multiple Diverse Counterexamples for an EFSM[END_REF], the authors present an approach relying on LTL model checking, which produces multiple counterexamples and which is able to reduce the number of counterexamples by detecting whether two counterexamples are equivalent. These approaches share similarities with our work because they focus on the generation of multiple counterexamples. Nevertheless, they do not exploit this result as we did for providing additional relevant information to developers such as the number of bugs or more precise counterexamples.

CONCLUDING REMARKS

In this paper, we have presented a solution for counting the number of bugs when analyzing a specification using model checking techniques. To do so, we focus on specific decision points in the specification, that make the corresponding model go to a correct or an incorrect portion of the model. These faulty choices are particularly helpful during the debugging task because they highlight the cause of the violation of a property. The approach relies on the counterexample LTS, which is an LTS consisting of all possible counterexamples. More specifically, we have proposed an algorithm to compute the number of bugs in the specification, which allows one to quantify how buggy is the specification and thus the effort required in the debugging phase. The main idea of this algorithm is to use some specific actions in the property to emphasize some parts of the specification that may cause its violation. Then, by comparing successive versions of the counterexample LTS, we manage to identify whether these suspicious pieces of the specification are actual bugs or not. Finally, the generation of counterexamples is possible from the final counterexample LTS. These counterexamples differ from regular ones because they include colored transitions and faulty states, and can be obtained using different strategies. The whole approach is fully automated by a tool we implemented and validated on several examples for validation purposes.

The main perspective of this work is to support liveness properties. In this case, counterexample LTSs and counterexamples have different shapes (lassos), and the approach thus deserves to be revisited, in particular the part comparing counterexamples LTSs.

Definition 2 . 1 .

 21 (LTS) An LTS is a tuple 𝑀 = (𝑆, 𝑠 0 , Σ,𝑇 ) where 𝑆 is a finite set of states, 𝑠 0 ∈ 𝑆 is the initial state, Σ is a finite set of labels, and 𝑇 ⊆ 𝑆 × Σ × 𝑆 is a finite set of transitions. A transition is represented as 𝑠 𝑙 -→ 𝑠 ′ ∈ 𝑇 , where 𝑙 ∈ Σ.

Definition 2 . 4 .

 24 (Tagged LTS) Given an LTS 𝑀 = (𝑆, 𝑠 0 , Σ,𝑇 ), and the set of transition tags Γ, the tagged LTS is a tuple 𝑀 𝑇 = (𝑆 𝑇 , 𝑠 0 𝑇 , Σ 𝑇 ,𝑇 𝑇 ) where 𝑆 𝑇 = 𝑆, 𝑠 0 𝑇 = 𝑠 0 , Σ 𝑇 = Σ, and

Definition 2 . 5 .

 25 (Faulty State) Given a tagged LTS 𝑀 𝑇 = (𝑆 𝑇 , 𝑠 0 𝑇 , Σ 𝑇 ,𝑇 𝑇 ), a state 𝑠 ∈ 𝑆 𝑇 is a faulty state if ∃𝑡 = 𝑠 ′ (𝑙,𝛾 ) ----→ 𝑠 ∈ 𝑇 𝑇 where 𝑡 is a neutral transition, and ∃𝑡 1 = 𝑠 (𝑙 1 ,𝛾 1 )

Figure 1 :

 1 Figure 1: Legend for Transitions, Faulty States, and States

Listing 1 :

 1 Example of LNT Specification

Figure 2 :

 2 Figure 2: Example of Counterexample LTS

Definition 3 . 2 .

 32 (Inevitable Bug) Given an LTS 𝑀 = (𝑆, 𝑠 0 , Σ,𝑇 ) and a property 𝑃, there is an inevitable bug in 𝑀 if 𝑡 ∈ 𝑡 (𝑀) such that 𝑡 |= 𝑃. Definition 3.3. (Avoidable Bug) Given an LTS 𝑀 = (𝑆, 𝑠 0 , Σ,𝑇 ) and a property 𝑃, there is an avoidable bug in 𝑀 if ∃ 𝑡, 𝑡 ′ ∈ 𝑡 (𝑀) such that 𝑡 |= 𝑃 and 𝑡 ′ ̸ |= 𝑃.

Definition 3 . 4 .

 34 (Dummy Choice) Given a specification 𝐿 and an action 𝐴 appearing in 𝐿, the addition of a dummy choice transforms 𝐴 into a choice statement (select construct in LNT) with two clauses: the first clause contains the action 𝐴 and the second clause contains a new action 𝐷𝑈 𝑀𝑀𝑌 which is not used anywhere in the specification 𝐿.

Figure 3 :

 3 Figure 3: Counterexample LTSs for Specifications in Listings 2 (a) and 3 (b)

Definition 3 . 5 .

 35 (Counterexample LTS Comparison) Given two counterexample LTSs 𝐶 = ((𝑆 𝑇 , 𝑠 0 𝑇 , Σ 𝑇 ,𝑇 𝑇 ), 𝐹 ) and 𝐶 ′ = ((𝑆 ′ 𝑇 , 𝑠 ′0 𝑇 , Σ ′

Figure 4 :

 4 Figure 4: Counterexample LTSs with Dummy Choices

Algorithm 1 : 8 if action ∈ A then 9 𝑑𝑢𝑚𝑚𝑦

 189 Algorithm for Counting Bugs Inputs : 𝐿 (LNT specification), 𝑃 (MCL property) Outputs : 𝑛 𝑎𝑣𝑑 , 𝑛 𝑖𝑛𝑣 ∈ N 1 -Step 1: addition of dummy choices -2 (𝑆, 𝑠 0 , Σ,𝑇 ) := 𝑔𝑒𝑛𝑒𝑟𝑎𝑡𝑒𝐿𝑇 𝑆 (𝐿); 3 𝑅 := 𝑔𝑒𝑡𝑅𝑒𝑔𝐸𝑥𝑝𝑟 (𝑃); 4 𝐴 := 𝑙𝑎𝑠𝑡 (𝑅, Σ); 5 𝐷 := ∅; 6 𝑐𝑜𝑢𝑛𝑡𝑒𝑟 := 1; 7 foreach 𝑎𝑐𝑡𝑖𝑜𝑛 in 𝑔𝑒𝑡𝐴𝑐𝑡𝑖𝑜𝑛𝑠 (𝐿) do := "𝑑𝑢𝑚𝑚𝑦" + 𝑐𝑜𝑢𝑛𝑡𝑒𝑟 ; 10 𝐿 := 𝑎𝑑𝑑𝐷𝑢𝑚𝑚𝑦𝐶ℎ𝑜𝑖𝑐𝑒 (𝑎𝑐𝑡𝑖𝑜𝑛, 𝑑𝑢𝑚𝑚𝑦, 𝐿); 11 𝐷 := 𝐷 ∪ {𝑑𝑢𝑚𝑚𝑦}; 12 𝑐𝑜𝑢𝑛𝑡𝑒𝑟 := 𝑐𝑜𝑢𝑛𝑡𝑒𝑟 + 1; 13 end 14 (𝑀 𝑇 , 𝐹 ) := 𝑔𝑒𝑛𝑒𝑟𝑎𝑡𝑒𝐶𝐿𝑇 𝑆 (𝐿, 𝑃); 15 -Step 2: identification of dummy choices corresponding to real bugs -16 𝐷 ′ := ∅; 17 foreach 𝑠 in 𝑔𝑒𝑡𝑆𝑡𝑎𝑡𝑒𝑠 (𝑀 𝑇 ) do 18 if (∃𝑡 = 𝑠 (𝑙,𝛾 ) ----→ 𝑠 ′ ∈ 𝑔𝑒𝑡𝑇𝑟𝑎𝑛𝑠 (𝑀 𝑇 ) s.t. 𝑙 ∈ 𝐷) and (𝑠 ∈ 𝐹 ) then 19 𝐷 ′ := 𝐷 ′ ∪ {𝑔𝑒𝑡𝐷𝑢𝑚𝑚𝑦𝐴𝑐𝑡𝑖𝑜𝑛(𝑠)}; 20 end 21 -Step 3: bug counting for each kind of bug -22 𝑛 𝑎𝑣𝑑 := 0; 23 𝑛 𝑖𝑛𝑣 := 0; 24 foreach 𝑑𝑢𝑚𝑚𝑦 in 𝐷 ′ do 25 𝐿 ′ := 𝐿; 26 𝐿 ′ := 𝑟𝑒𝑚𝑜𝑣𝑒𝐷𝑢𝑚𝑚𝑦𝐶ℎ𝑜𝑖𝑐𝑒 (𝑑𝑢𝑚𝑚𝑦, 𝐿 ′ ); 27 (𝑀 ′ 𝑇 , 𝐹 ′ ) := 𝑔𝑒𝑛𝑒𝑟𝑎𝑡𝑒𝐶𝐿𝑇 𝑆 (𝐿 ′ , 𝑃); 28 if 𝐹 ′ ≠ ∅ then 29 𝑛 𝑎𝑣𝑑 := 𝑛 𝑎𝑣𝑑 + 1; 30 if 𝐹 ′ = ∅ then 31 𝑛 𝑖𝑛𝑣 := 𝑛 𝑖𝑛𝑣 + 1; 32 end 33 return 𝑛 𝑎𝑣𝑑 , 𝑛 𝑖𝑛𝑣 ;

1 p r oListing 4 :

 4 c e s s Main [ INIT , EXEC , CLOSE , AA, BB , CC : any ] LNT Specification with Several Bugs

Figure 5 :

 5 Figure 5: Counterexample LTS before (a) and after (b) Addition of Dummy Choices

Figure 6 :

 6 Figure 6: Iterations in the Final Step of the Bug Quantification Algorithm

Figure 7 :

 7 Figure 7: Final Counterexample LTS

Figure 8 :

 8 Figure 8: Shortest Counterexample

Figure 9 :

 9 Figure 9: Tool Support

Table 1 :

 1 𝐴 𝑚 in 𝐵 1 ||...||𝐵 𝑛 end par | 𝑃 [𝐴 1 , ..., 𝐴 𝑚 ] (𝐸 1 , ..., 𝐸 𝑛 ) | while 𝐸 loop 𝐵 end loop | var 𝑥:𝑇 in 𝑥 := 𝐸; 𝐵 end var Excerpt of LNT Syntax (Behaviour Part)

Table 2 :

 2 Experiments on Realistic Examples

FormaliSE'22, May 18-22, 2022, Pittsburgh, PA, USA Irman Faqrizal and Gwen Salaün

Assume a property defined as follows: [𝐴. (𝐵 ∧ 𝐶 ) ] 𝑓 𝑎𝑙𝑠𝑒. This property is true on all LTS models. This comes from the 𝐵 ∧ 𝐶 predicate, which is always false since 𝐵 and 𝐶 are different actions names (i.e., no label of an LTS can satisfy 𝐵 and 𝐶). Since the predicate 𝐵 ∧ 𝐶 is false, the regular formula 𝐴. (𝐵 ∧ 𝐶 ) does not match any transition sequence in any LTS, so the modality (which expresses the absence of such sequences) always evaluates to true.


Wojciech Kazana
email: kazana@lsv.ens-cachan.fr

Luc Segoufin

FIRST-ORDER QUERY EVALUATION ON STRUCTURES OF BOUNDED DEGREE

Keywords: 1998 ACM Subject Classification: F.4.1, F.1.3 First-order, query evaluation, enumeration, constant delay

 it was shown that this problem is in Constant-Delay lin . An enumeration problem belongs to Constant-Delay lin if for an input of size n it can be solved by:

• an O(n) precomputation phase building an index structure,

• followed by a phase enumerating the answers with no repetition and a constant delay between two consecutive outputs. In this article we give a different proof of this result based on Gaifman's locality theorem for first-order logic. Moreover, the constants we obtain yield a total evaluation time that is triply exponential in the size of the input formula, matching the complexity of the best known evaluation algorithms.

Introduction.

Model checking is the problem of testing whether a given sentence is true in a given model. It's a classical problem in many areas of computer science, in particular in verification. If the formula is no longer a sentence but has free variables then we are faced with the query evaluation problem. In this case the goal is to compute all the answers of a given query on a given database.

As for model checking, query evaluation is a problem often requiring a time at least exponential in the size of the query. Even worse, the evaluation often requires a time of the form n O(k) , where n is the size of the database and k the size of the query. This is dramatic, even for small k, when the database is huge.

However there are restrictions on the structures that make things easier. For instance MSO sentences can be tested in time linear in n over structures of bounded tree-width [START_REF] Courcelle | Graph Rewriting: An Algebraic and Logic Approach[END_REF] and MSO queries can be evaluated in time linear in n + m, where m is the size of the output of the query (note that m could be exponential in the number of free variables of the query, and hence in k) [START_REF] Flum | Query evaluation via tree-decompositions[END_REF].

In this paper we are concerned with first-order logic (FO) and structures of bounded degree. In this case the model checking problem for FO sentences is known to be linear in n [START_REF] Seese | Linear Time Computable Problems and First-Order Descriptions[END_REF]. Moreover, the constant factor is at most triply exponential in the size k of the formula [START_REF] Frick | The complexity of first-order and monadic second-order logic revisited[END_REF]. This last algorithm easily extends to query evaluation obtaining an algorithm working in time f (k)(n + m) where f is a triply exponential function.

As we already mentioned, the size m of the output may be exponential in the arity of the formula and therefore may still be large. In many applications enumerating all the answers may already consume too many of the allowed resources. In this case it may be appropriate to first output a small subset of the answers and then, on demand, output a subsequent small number of answers and so on until all possible answers have been exhausted. To make this even more attractive it is preferable to be able to minimize the time necessary to output the first answers and, from a given set of answers, also minimize the time necessary to output the next set of answers -this second time interval is known as the delay.

We say that a query can be evaluated in linear time and constant delay if there exists an algorithm consisting of a preprocessing phase taking time linear in n which is then followed by an output phase printing the answers one by one, with no repetition and with a constant delay between each output. Notice that if a linear time and constant delay algorithm exists then the time needed for the total query evaluation problem is bounded by f (k)(n + m) for some function f . Hence this is indeed a restriction of the linear time query evaluation algorithms mentioned above. From the best of our knowledge it is not yet known whether a bound f (k)(n + m) for some function f on a query evaluation problem implies the existence of a linear time and constant delay enumeration algorithm. We conjecture this is not the case.

It was shown in [START_REF] Durand | First-order queries on structures of bounded degree are computable with constant delay[END_REF] that linear time constant delay query evaluation algorithms could be obtained for FO queries over structures of bounded degree, hence improving the results of [START_REF] Seese | Linear Time Computable Problems and First-Order Descriptions[END_REF] and [START_REF] Frick | The complexity of first-order and monadic second-order logic revisited[END_REF].

The proof of [START_REF] Durand | First-order queries on structures of bounded degree are computable with constant delay[END_REF] is based on an intricate quantifier elimination method. In this paper we provide a different proof of this result based on Gaifman Locality of FO queries. Our algorithm can be seen as an extension of the algorithm of [START_REF] Frick | The complexity of first-order and monadic second-order logic revisited[END_REF] to queries. However the index structure built during the preprocessing phase is more complicated than the one of [START_REF] Frick | The complexity of first-order and monadic second-order logic revisited[END_REF] in order to obtain the constant delay enumeration. Moreover, our constant factor is triply exponential in the size of the formula, while it is not clear whether the constant factor obtained in [START_REF] Durand | First-order queries on structures of bounded degree are computable with constant delay[END_REF] is elementary. Note that the triply exponential constant factor cannot be significantly improved: it is shown in [START_REF] Frick | The complexity of first-order and monadic second-order logic revisited[END_REF] that a constant factor only doubly exponential in the size of the formula is not possible unless the parametrized complexity class AW[ * ] collapses to the parametrized class FPT.

Definitions.

2.1. Gaifman locality and first-order logic. A relational signature is a tuple σ = (R 1 , . . . , R l ), each R i being a relation symbol of arity r i . A relational structure over σ is a tuple A = A, R A 1 , . . . , R A l , where A = {a 1 , . . . , a m } is the set of elements of A and R A i is a subset of A r i . We fix a reasonable encoding of structures by words over some finite alphabet. The size of A is denoted by ||A|| and is the length of the encoding of A.

The Gaifman graph of a relational structure A, denoted by G(A), is defined as follows: the set of vertices of G(A) is A and there is an edge (a, b) in G(A) iff there exists a relation R i and a tuple t ∈ R i such that both a and b occur in t. Given a, b ∈ A, the distance between a and b, denoted δ(a, b), is the length of a shortest path between a and b in G(A) or ∞ if a and b are not connected. The distance between two tuples ā = (a 1 , . . . , a k ) and b = (b 1 , . . . , b l ) of A, denoted δ(ā, b), is the min{δ(a i , b j ) : 1 ≤ i ≤ k, 1 ≤ j ≤ l}. For a given r ∈ N and a given tuple of elements ā of some structure A, we denote by N r (ā) the set of all elements in A such that their distance from ā is less or equal to r. The r-neighborhood of ā, denoted as N r (ā), is the substructure of A induced by N r (ā) and expanded with one constant for each element of ā. Given two tuples of elements ā and b we say that they have the same r-neighborhood type, written N r (ā) N r ( b), if there is an isomorphism between N r (ā) and N r ( b).

We consider first-order logic (FO) built from atomic formulas of the form x = y or R i (x 1 , . . . , x r i ) for some relation R i and closed under the usual Boolean connectives (¬, ∨, ∧) and existential and universal quantifications (∃, ∀). When writing φ(x) we always mean that x are exactly the free variables of φ. Given a structure A and a tuple ā of elements of A, we write A |= φ(ā) if the formula φ is true in A after replacing its free variables with ā. As usual |φ| denotes the size of φ.

We are now ready to state Gaifman locality for FO.

Theorem 2.1 (Gaifman Locality Theorem [START_REF] Libkin | Elements of Finite Model Theory[END_REF]). For any first-order formula φ(x), for every structure A and tuples ā, b, we have

N r (ā) N r ( b) implies A |= φ(ā) iff A |= φ( b), where r = 2 |φ| .
Given d ∈ N, a structure is said to be d-degree-bounded, if the degree of the Gaifman graph is bounded by d. The following nice algorithmic property of d-degree-bounded structures can be proved using Theorem 2.1.

Theorem 2.2 ([9, 5]). Fix d ∈ N. The problem of whether a given d-degree-bounded structure A satisfies a given first-order sentence φ is decidable in time 2 2 2 |φ| O(1)
||A||.

2.2.

Model of computation and Constant-Delay lin class. We use Random Access Machines (RAM) with addition and uniform cost measure as a model of computation. For further details on this model and its use in logic see [START_REF] Durand | First-order queries on structures of bounded degree are computable with constant delay[END_REF].

An enumeration problem is a binary relation. Given an enumeration problem R and an input x, a solution for x is a y such that (x, y) ∈ R. An enumeration problem R induces a computational problem as follows: Given an input x, output all its solutions. An enumeration problem is in the class Constant-Delay lin if on input x it can be decomposed into two steps:

• a precomputation phase that is performed in time O(|x|),

• an enumeration phase that outputs all the solutions for x with no repetition and a constant delay between two consecutive outputs. The enumeration phase has full access to the output of the precomputation phase but can use only a constant total amount of extra memory. In particular if R is in Constant-Delay lin then the enumeration problem R can be solved in time O(|x| + |{y : R(x, y)}|). From the best of our knowledge it is not known whether the converse is true or not. We conjecture that it is not. More details about Constant-Delay lin can be found in [START_REF] Durand | First-order queries on structures of bounded degree are computable with constant delay[END_REF].

We are interested in the following enumeration problem for φ(x) ∈ FO and d ∈ N:

Enum d (φ) = {(x, y) : x is a d-degree-bounded structure A, y is a tuple ā of elements of A and A |= φ(ā)}
We further denote by φ(A) the set {ā : A |= φ(ā)} and by |φ(A)| the cardinality of this set. We show that Enum d (φ) is in Constant-Delay lin .

Theorem 2.3 ([3]

). There is an algorithm that for all d ∈ N, all φ ∈ FO and all d-degreebounded structures A enumerates φ(A) with a precomputation phase taking time

2 2 2 |φ| O(1)
•||A|| and a delay during the enumeration phase that is triply exponential in |φ|. In particular, for all d ∈ N and all φ ∈ FO the enumeration problem Enum d (φ) is in Constant-Delay lin . Moreover, if the domain of A is linearly ordered, the algorithm enumerates φ(A) in increasing order relative to the induced lexicographical order on tuples.

Hence the total query evaluation induced by the enumeration procedure of Theorem 2.3 is in time 2 2 2 |φ| O (1) (||A|| + |φ(A)|) thus matching the model checking complexity of Theorem 2.2. Our proof of Theorem 2.3 is based on Gaifman Locality Theorem while the proof of [START_REF] Durand | First-order queries on structures of bounded degree are computable with constant delay[END_REF] uses a quantifier elimination procedure (see also [START_REF] Lindell | A Normal Form for First-Order Logic over Doubly-Linked Data Structures[END_REF] for a similar argument). Note that it is not clear from the proof of [START_REF] Durand | First-order queries on structures of bounded degree are computable with constant delay[END_REF] that their algorithm is triply exponential in the size of the formula.

FO query evaluation.

In this section we assume d ∈ N to be fixed and all our structures are d-degree bounded. A formula φ(x) with k free variables x = x 1 . . . x k is said to be connected around x 1 if φ(x) logically implies that x 2 , . . . , x k are in the (rk)-neighborhood of x 1 for r = 2 |φ| .

Let T rk be the set of all isomorphism types of (rk)-neighborhoods of single elements, i.e. the isomorphism types of structures of the form N rk (a) for some element a of some structure A. By (rk)-neighborhood-type of an element a we mean the isomorphism type of its (rk)-neighborhood. Because our structures are d-degree-bounded each (rk)-neighborhood has at most d rk elements. For each τ ∈ T rk we denote by µ τ (x) the fact that the (rk)neighborhood-type of x is τ . For each type in T rk we fix a representative for the corresponding (rk)-neighborhood and fix a linear order among its elements. This way, we can speak of the first, second,. . . , element of an (rk)-neighborhood. For technical reasons, we actually fix a linear order for each l-neighborhood for l ≤ rk such that (i) it is compatible with the distance from the center of the neighborhood: the center is first, then come all the elements at distance 1, then all elements at distance 2 and so on. . . and (ii) the order of a (l + 1)-type is consistent with the order on the induced l-type.

For some sequence F = {α 2 , . . . , α m } of (m -1) elements from [1, . . . , d rk ], we write x = F (x 1 ) for the fact that, for j ∈ {2, . . . , m}, x j is the α j -th element of the (rk)-neighborhood of x 1 . Let F m rk be the set of all possible such F . Let

F rk = 1≤m≤k F m rk . For a given x = x 1 . . . x k a r-partition of x is a set of pairs {(C 1 , F 1 ), . . . , (C m , F m )} such that ∅ = C i ⊆ x, 1≤i≤m C i = {x 1 , . . . , x k }, C i ∩ C j = ∅ for i = j, and F i ∈ F |C i |
rk . For a given r-partition C of x and (C i , F i ) ∈ C we write xi to represent variables from C i , x i 1 to represent the first variable from C i , x i 2 to represent second variable and so on. For a given r-partition C = {(C 1 , F 1 ), . . . , (C m , F m )} of x by Div C r (x) we mean a conjunction of formulas saying that N r (x i ) ∩ N r (x j ) = ∅ for all 1 ≤ i = j ≤ m and formulas

(C i ,F i )∈C xi = F i (x i 1 )
. Note that the latter part implies that xi is connected around x i 1 . The following is an immediate consequence of Theorem 2.1. Lemma 3.1. Fix a structure A. Then any formula φ(x) with k free variables is equivalent over A to a formula of the form

C∈Cr(x)   Div C r (x) ∧ (τ 1 ,...,τ |C| )∈S C i≤|C| µ τ i (x i 1 )   (3.1)
where r = 2 |φ| , C r (x) is the set of all r-partitions of x, and S C ⊆ (T rk ) |C| is finite.

Proof. Let φ(x) be a formula with k free variables and r = 2 |φ| . As in the statement of this lemma, we denote by C r (x) the set of all partitions C = {(C 1 , F 1 ), . . . , (C m , F m )} of x with

C i = x i 1 , . . . , x i |C i |
. By taking all possible r-partitions over x we see that φ(x) is equivalent to:

C∈Cr(x) Div C r (x) ∧ φ(x)
Let ā be a tuple of A such that A |= φ(ā). Thus there exists C ∈ C r (x), such that A |= Div C r (ā) ∧ φ(ā). As Div C r induces that variables from each C i for some (C i , F i ) ∈ C are connected, the r-neighborhood of each āi is completely included into the (rk)-neighborhood of a i 1 . Let m = |C|. For 1 ≤ i ≤ m let τ i be the rk-neighborhood-type of a i 1 . We now take S C as the set of all such tuples (τ 1 , . . . , τ m ) for all tuples ā and all r-partitions C such that A |= Div C r (ā) ∧ φ(ā). By construction we have φ(x) implies (3.1). The reverse inclusion is an immediate consequence of Gaifman Locality Theorem: When Div C r (ā) holds, N r (ā i ) is induced by N rk (a i 1 ) = τ i and F i . Moreover, N r (ā) is the disjoint union of N r (ā i ) and is therefore induced by C.

We are now ready to prove Theorem 2.3.

Proof of Theorem 2.3. Fix a formula φ(x) with k free variables. Let A be a structure. Let r = 2 |φ| . By Lemma 3.1, φ(x) is equivalent over A to a formula of the form given by (3.1). We assume that A comes with a linear order over its elements. If not, we use the linear order induced by the encoding of A.

Intuitively the precomputation phase determines the disjunction given by (3.1) and precomputes the (rk)-neighborhoods of each element of A. The fact that this can be done in time linear in ||A|| and triply exponential in |φ| will make use of Theorem 2.2.

In a first step, for each i ≤ rk we precompute the pairs of nodes at distance i. In other words, for each a in A, we compute the set of elements b such that δ(a, b) = i. This can easily be done in time linear in rk • ||A|| by induction on i: during the base case we compute the Gaifman graph of A and then we perform the classical computation of the transitive closure of this graph up to depth rk.

In a second step, the precomputation phase computes for each element a of A its (rk)neighborhood: for each element a of A, we compute its (rk)-neighborhood-type and for all i ≤ d rk a pointer from a to the i-th element of its (rk)-neighborhood. We use an induction on the radius of the neighborhood to achieve this goal within the desired time constraints.

As 0-neighborhoods all share the same isomorphism type and have just one pointer to their centers, the induction base is obvious. So let's assume that in linear time in the size of A we have computed all l-neighborhoods for all nodes. With one more linear pass we now compute the (l + 1)-neighborhoods. Fix a ∈ A. From the first step, we have all the elements of A at distance l + 1 from a. As we already have computed the l-neighborhood, it remains to try all possible orders among those elements and test isomorphism with the ordered types we have initially fixed.

There are at most d l+1 nodes at distance l + 1 and l < rk. Hence the number of orders we need to test is bounded by (d rk )!. Once the order is fixed we try all possible (rk)neighborhood-types that we have initially fixed (there are |T rk | possibilities) and then test that the two orders induce an isomorphism (each test simply requires going through all tuples of the neighborhood). Let s(r, k, d) be the maximal size of a (rk)-neighborhood. Thus this step is altogether achieved in time O((

d rk )! • |T rk | • s(r, k, d)) which is triply exponential in |φ| because r = 2 |φ| , |T rk | = O(2 s(r,k,d) ) and s(r, k, d) = O(d rk|σ| ).
During the third step of the precomputation we determine the (rk)-neighborhood-types that are relevant for φ over A. Fix a r-partition C = {(C 1 , F 1 ), . . . , (C m , F m )} of C r (x) and a sequence τ 1 , . . . , τ m ∈ T rk . This sequence is relevant for C if A |= ∃x Div C r (x) ∧ j µ τ j (x j 1 ) ∧ φ(x). Notice that the tests of the form µ τ j (x j 1 ) have been precomputed during the second step and can therefore now be treated as unary symbols. Similarly the tests Div C r (x) can be expressed using the graph computed during the first phase. Altogether, the first and second phase has replaced Div C r (x) ∧ j µ τ j (x j 1 ) with a formula of size polynomial in k. Hence we can apply Theorem 2.2 in order to test whether the sequence is relevant for C in time linear in ||A|| and triply exponential in the size of the formula. We do this for all possible C,

investigating at most (|T rk |) k = 2 2 2 O(|φ|)
cases. The number of possible C is the number of possible splits of k variables into disjoint and nonempty subsets multiplied by (|F rk |) k , which altogether is again 2 2 2 O(|φ|) . For each C we store a list of all sequences relevant for it. We call a r-partition C relevant if that list is nonempty.

The fourth step of the precomputation phase orders, for each τ ∈ T rk , the elements of A having that particular (rk)-neighborhood-type and stores a pointer from one element to the next one according to the linear order on the elements of A. To do that, we just need to enumerate through all the elements in A, in the order provided by the linear order on its elements, and, using information obtained in the second step, add each of them to a proper list. In order to do this we need to be able to sort a set of elements in linear time and this can be done in our RAM model as explained in [START_REF] Grandjean | Sorting, Linear Time and the Satisfiability Problem[END_REF].

The rest of the proof is an induction on the number k of free variables in φ.

Fix relevant r-partition C = {(C 1 , F 1 ), . . . , (C m , F m )} in C r (x). We show how to enumerate in lexicographical order, with no repetition, constant memory and constant delay, all the tuples ā such that A, ā |= Div C r (x) ∧ i j µ τ ij (x ij 1 ). The result will then follow from the following simple lemma, whose proof consist in merging two ordered lists.

Lemma 3.2 ([1]

). If there is a linear order < such that R, R are in Constant-Delay lin and both output their answers in increasing order relative to <, then R ∪ R is also in Constant-Delay lin and the answers can be enumerated in increasing order relative to <.

The base case k = 1 is trivial: since k = 1, it must be the case that also m = 1 and recall that the fourth step of the precomputation phase already computed the desired list of all elements of type τ 1 . Assume now that we have the desired enumeration procedure for formulas with less than k free variables and we want to extend it to the ones with k free variables.

Without loss of generality assume that the most significant variable of x is in the first variable of x1 , that the most significant variable of x \ x1 is the first variable of x2 and so on.

Let x = C 1 ∪ . . . ∪ C m-1 and x = C m . Consider query ψ(x ) = ∃x Div C r (x) ∧ i j µ τ ij (x ij 1
). It has less free variables than φ and so the inductive hypothesis holds for it.

The last step of the precomputation phase performs the precomputation phase as given by the inductive hypothesis for ψ.

Altogether we have a precomputation phase of the desired properties: it works in time linear in |A| and triply exponential in |φ|. We now turn to the enumeration phase.

We simultaneously do the following for each sequence τ 1 , . . . , τ m relevant for C and use Lemma 3.2 to avoid duplicate answers.

Fix τ 1 , . . . , τ m relevant for C. We enumerate, by induction, the solutions for ψ and recall that ψ implies Div C r (x) ∧ i j µ τ ij (x ij 1 ), where C is C with (C m , F m ) removed. For each solution b obtained by induction, using the precomputed pointers, we nest the enumeration of all elements a m of A whose (rk)-neighborhood-type is τ m . For each such element let ām = F m (a m ). Given a m whose (rk)-neighborhood-type is τ m , we check whether N r (ā m ) intersects with N r ( b) or not (recall that this information has been precomputed during the first phase and therefore requires only constant time). If it does not, we have a solution b, ām for φ because of (3.1). If it does then we move to the next element whose (rk)-neighborhoodtype is τ m . Notice that the size of N r ( b) is bounded by kd r and ām is r-connected around a 1 (thus included in N rk (a m )), hence the length of false hits is bounded by kd r(k+1) . From the definition of ψ, for each b we are certain to find at least one matching ām that gives us a solution b, ām to φ. Altogether we get the desired constant delay for the enumeration process.

The enumeration phase needs to process all possible r-partitions C and all relevant sequences of T rk , i.e. a number of cases triply exponential in |φ|. For a fixed sequence τ 1 , . . . , τ m relevant for C the output is clearly returned in lexicographical order and Lemma 3.2 justifies that it is also the case for the enumeration procedure for φ. Altogether this yields a procedure linear in the size of the output and triply exponential in |φ|.

Conclusion

We have given a new proof of the linear time and constant delay enumeration problem of first-order queries over structures of bounded degree. Our procedure is based on Gaifman's

Acknowledgement

The authors wish to thank Dietrich Kuske and the anonymous referees for their constructive comments on earlier versions of this paper.

This work has been partially funded by the European Research Council under the European Community's Seventh Framework Programme (FP7/2007-2013) / ERC grant Webdam, agreement 226513. http://webdam. inria.fr/ . We acknowledge the financial support of the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under the FET-Open grant agreement FOX, number FP7-ICT-233599. and L. Segoufin Creative Commons

locality theorem for first-order logic and our constants are triply exponential in the size of the query, and therefore induces the known complexity of the associated model checking problem.