# Incremental Formula-Based Fix Localization
## 3 Proposed Method
### Overall Fault Localization Algorithm  
The overall fault localization process of AgxFaults is described in Algorithm 1. In the algorithm, \(P_{ggx}\) represents the dynamic control flow graph of the angelic program, and \(solver\) is an instance of an Incremental Partial MaxSat Solver. Additional hard and soft constraints can be added into the solver via method _addHard()_ and _addSoft()_, respectively. The method _Check()_ of the solver returns _True_ if it finds an MCS for the current formula; otherwise, it returns _False_.  
In the beginning, the algorithm initializes \(P_{ggx}\) as a pure angelic program (which does not contain any specific statements, line 1). The formula solver, \(solver\), is initialized with the set of soft-constraints empty and the set of hard-constraints containing clauses encoding the test input and its assertion (lines 1 to 3).  
The main process of the algorithm is the loop from line 4 to line 15. It is an iterative process comprising the following steps: At the beginning of each iteration, it asks the solver to find an MCS for the current formula, line 4. If there is no more MCS, then the loop is terminated. Otherwise, the iteration starts and the solution of the formula is stored in \(model\), line 5. Then, based on \(model\), it determines the corresponding possible faulty statements \(mcs\) and an angelic execution \(\Pi_{qgx}\) in the angelic program, line 6. If the angelic execution \(\Pi_{qgx}\) contains unspecified executions (i.e., the if condition at line 7 is true), then the angelic refinement process is performed to refine the angelic program and angelic formula at these angelic-branches, line 8. Otherwise, \(\Pi_{qgx}\) is a feasible angelic execution; thus, the possible fault location \(mcs\), together with the angelic execution path \(\Pi_{qgx}\), are reported to the developer, line 12. In addition, a blocking constraint is added to the solver, line 13. This blocking constraint guarantees that the current MCS will not be encountered again in subsequent iterations. Specifically, the blocking constraint of the  
Figure 4: Overview of AgxFaults.  
MCS is \(\bigvee\{c|c\in mcs\}\). The blocking constraint states that all program statements in the \(mcs\) are not simultaneously containing faults.  
```
0:\(prog\): buggy program
0:\((inp\),as): failing test case
0:bound: maximum bound fix location size
0:\(\{\)(stmt,angelic correct execution)\(\}\)
1:\(P_{qgx},IN,AS\leftarrow\mathcal{O},inp,as\)
2:\(\Phi_{h},\Phi_{s}\leftarrow(IN\cup AS),\mathcal{O}\)
3:\(solver\) = new IncrMaxSMISolver(\(\Phi_{h},\Phi_{s},bound\));
4:while\(solver.Check()\wedge\
eg timeout()\)do
5:\(\varphi_{mcs},model\gets solver.\)getModel()
6:\(stmt,\Pi_{qgx}\leftarrow\)AnalyzeMCS(\(model\), \(P_{qgx}\))
7:if(\(\Pi_{qgx}\) contain angelic-branches) then
8:\(P_{qgx},\Phi_{h},\Phi_{s}\leftarrow\)AngelicRefinement(\(stmt,\Pi_{qgx},P_{qgx}\))
9:\(solver.\)addHard(\(\Phi_{h}\))
10:\(solver.\)addSoft(\(\Phi_{s}\))
11:else
12:writeOutput(\(stmt\),\(\Pi_{qgx}\))
13:\(solver.\)addHard(BlockingConstraint(\(\varphi_{mcs}\)))
14:endif
15:endwhile
```  
**Algorithm 1** Overall Fault Localization Algorithm