In this paper I explore a further option for solving B constraints. In particular, I develop a framework translating B predicates to s(CASP), a goal-directed form of Answer Set Programming. Furthermore, the presented framework implements an interface enabling B predicates to be solved by the s(CASP) engine within the ProB tool as an additional backend. This paper particularly focuses on the translation process and on empirically evaluating the framework's performance by comparing it to the native, Kodkod and Z3 backend of ProB. This work poses a foundation for future development regarding the translation of B predicates to goal-directed Answer Set Programming and s(CASP) speci cally. Further, this framework can be used to aid the veri cation of other solvers' correctness.
This work's fundamental motivation is to develop zero-defect software with the
help of formal methods. For instance, this is achievable by specifying a system's
desired behavior with B abstract machines [
In this paper I aim towards extending the existing base of constraint solvers
for the B-Method, used in the ProB tool, by providing an additional constraint
solving backend. In particular, this work implements a Prolog framework
translating B predicates to Answer Set Programming [
Copyright c 2021 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
Answer Set Programming (ASP) is a form of declarative logic programming,
which is primarily oriented towards NP-hard search problems [
s(CASP) [
This framework consists of a translator and an interface. The translator obtains
an abstract syntax tree (AST) representing a B predicate emitted by ProB and
generates semantically equivalent s(CASP) code. It is written in SICStus Prolog [
The overall work ow is illustrated in Figure 1. An AST is expected as input by the framework, hence ProB parses the predicate prior to the translation. This initial process is depicted as a black box in the owchart. Thereafter, the translator generates a s(CASP) le containing executable code. The translator gradually walks over the AST and computes for each encountered B node a semantically equivalent s(CASP) component. Through this process a s(CASP) program is recursively build. When the generation of the translation is completed, the interface calls the s(CASP) engine and obtains the result. Lastly, some post-processing is applied and the result is returned back to ProB. In this section I give an overview of the translation process. The following designations are used for B code throughout this translation. Designations P, Q denote predicates; E, F denote expressions; x, y denote single variables; z denotes a list of variables; S, D denote set expressions; U denotes a set of sets and m, n denote integer expressions. Furthermore, for any B code A, TA denotes the translation of A in s(CASP). For the sake of simplicity the designations of B identi ers are also used for their s(CASP) representatives. For a B expression E the variable VE is uni ed with the evaluation of TE. Lastly, Tmp denotes a fresh internal temporary variable.
The vast majority of B predicates is covered. However, a few restrictions are introduced as this framework is still under development. Predicates such as set summation, set product, iteration, closure, projection, lambda abstraction and the support of sequences are not incorporated. Furthermore, in nite domains of the form a 2 N or b 2 Z are not considered. Lastly, in pure logic the order of P and Q is irrelevant for the semantics of a conjunction. However, conjunctions are currently straightforwardly translated. Therefore, the case that a ground value is needed for evaluating TP, which remains unbound until TQ is evaluated, is generally not supported. Nevertheless, s(CASP)'s CLP library allows for supporting arithmetical expressions.
Primitive expressions: Identi ers, booleans, integers and strings are straightforwardly translated.
Conjunction: P & Q is translated to TP, TQ.
Disjunction: P or Q introduces a goal subconst(x1,...,xk) with x1,...,xk being the variables occurring in P and Q. For both predicates a new rule is added to the code with the aforementioned goal as its head and with TP, TQ as its body respectively. Hence, the new goal establishes a choice point, e ectively creating a disjunction.
Negation: Let x1,...,xk be the variables occurring in P. not P introduces the goal not subconst(x1,...,xk) with the rule of the form subconst(x1,...,xk) :- TP.
Implication: P => Q is resolved as not P or Q.
Equivalence: P <=> Q is resolved as P => Q & Q => P.
Existential quanti cation: By virtue of s(CASP) operating query-driven, #(z).(P & Q) can be resolved as P & Q.
Equality, inequality and comparison operators: This translation applies to the operators =; 6=; <; >; ; . Without loss of generality, equality is selected to describe how the aforementioned operators are translated. As E = F may contain nested expressions or function calls the translator analyzes the AST to gather information about E and F. The translator operates with a look-ahead of one and introduces an internal temporary variable Ve if necessary. Depending on E and F the framework distinguishes between the following cases. 1. If E and F are primitive: TE = TF. 2. If E is primitive and F is not: TF, TE = VF. 3. If E is non-primitive and F is primitive: TE, VE = TF. 4. If E and F are both non-primitive: TE, TF, VE = VF.
Furthermore, the operators 6=; <; >; ; are translated to \=, #<, #>, #=<, #>= respectively. Thus, in case of arithmetical expressions s(CASP)'s CLP backend takes care of the aforementioned temporal challenges related to conjunctions. Empty set: Sets are represented by lists, hence fg is translated to []. Singelton set: Similar to equality, for a singleton set of the form fEg the translator analyzes E to decide whether the expression is primitive. Consequently, the translator produces Tmp = [TE] if E is primitive and TE, Tmp = [VE] vice versa. Via uni cation the framework takes care to link the freshly introduced temporary variable to the identi er or expression it is meant to be assigned to. Set enumeration: A set of arbitrary cardinality of the form fE, F, ...g follows the pattern of the singleton set, which is expressed by recursive application. Ordered pair: The framework distinguishes between four cases for an ordered pair E |-> F. 1. If E and F are primitive: Tmp = t(TE, TF). 2. If E is primitive and F is not: TF, Tmp = t(TE, VF). 3. If E is non-primitive and F is primitive: TE, Tmp = t(VE, TF). 4. If E and F are both non-primitive: TE, TF, Tmp = t(VE, VF). Set comprehension: Let x1,...,xi be all variables occurring in P and let z = z1,...,zj be the list of variables constrained by P. Let y1,...,yk with i = j+k denote external variables that occur in P but not in z. The set comprehension fz|Pg is the set of every value of z that satis es P and is translated to the goal subconst1(Tmp, y1,...,yk). Figure 2 shows the two introduced rules. subconst1/k+1 creates a local scope, where the variables of z are unable to clash with the variables of the parent scope. s(CASP)'s built-in predicate findall/3 is used to store in Tmp every instance of satisfying the condition TP. is an ordered pair of the form t(z1, t(z2, t(..., zj))) or scalar if |z| = 1. s u b c o n s t 1 (Tmp, y1,...,yk ) :
f i n d a l l ( , s u b c o n s t 2 ( x1,...,xi ) , Tmp) .
s u b c o n s t 2 ( x1,...,xi ) : TP . Universal quanti cation: Let z = z1,...,zk be the list of variables constrained by P. Further, let p1,...,pi and q1,...,qj be the external variables that occur in P and Q respectively but do not occur in z. The predicate !(z).(P => Q) is translated to subconst1(p1,...,pi, q1,...,qj). As this framework is restricted to nite domain declarations, it allows for using set comprehensions to express that Q is satis ed for each value of z satisfying P. Figure 3 depicts the three freshly introduced rules, where 's de nition is the same as for set comprehensions.
Fig. 3: The three introduced rules for the universal quanti cation predicate. Arithmetical evaluation: This translation applies to the arithmetical operators +; ; ; =; mod . Without loss of generality, addition is selected to describe how the aforementioned operators are translated. s(CASP)'s CLP library is used in order to omit temporal restraints of conjunctions. The predicate #=/2, which subsumes and extends is/2, is used instead. The framework distinguishes between four cases for m + n. 1. If m and n are primitive: Tmp #= Tm + Tn. 2. If m is primitive and n is not: Tn, Tmp #= Tm + Vn. 3. If m is non-primitive and n is primitive: Tm, Tmp #= Vm + Tn. 4. If m and n are both non-primitive: Tm, Tn, Tmp #= Vm + Vn.
Union: S \/ D is translated to TS, TD, union(VS, VD, Tmp). Except for the predicates genreal union and general intersection all other predicates are translated in the same way as union, i.e. intersection, di erence, cartesian product, powerset, cardinality, (not) member, (not) (strict) subset, minimum, maximum, interval, relations, domain, range, composition, identity, domain/range restriction/subtraction, inverse, relational image, override, direct/parallel product, partial/total functions/injections/surjections, bijections and function application. For predicates of arity two, merely the translation of one of the arguments is omitted. The corresponding predicates are provided in an external le1. General union & general intersection: Essentially, the translator stacks successively as many union/3 calls as necessary to compute the generalized union of the form union(U). The code for a general intersection inter(U) is generated analogously. The framework distinguishes between three cases. 1. If U = fSg, then resolve S as a singleton set. 2. If U = fS, Dg, then treat it as S \/ D. 3. If n 3, then resolve S1, S2 2 U as S1 \/ S2 obtaining Tmp1 and continue resolving Tmpi and the next set Si+2 with i < n-1 as TSi+2 , union(Tmpi, VSi+2 , Tmpi+1) until the nal result Tmpn-1 is computed. 5
In this section I aim towards empirically evaluating the presented framework's capabilities by comparing benchmark performances of the new backend to the native ProB, Kodkod and Z3 backend. Regarding the translation's correctness test cases are embedded in ProB consisting of numerous exemplary expressions, which cover the supported predicates. For each test the s(CASP) backend rst solves the underlying predicate obtaining a result, which is afterwards validated by ProB. Of course, this does not prove the backend's correctness.
In Figure 4 the runtime performances for the supported B predicates are presented. The result for a benchmark is obtained by solving and measuring the 1 https://github.com/Alexandros31/B-to-sCASP/blob/main/preliminaries.pl runtime of three separate synthetic B expressions on each backend (if available) via the ProB REPL. Additionally, the runtime of the plain s(CASP) engine is measured to gain more insight into s(CASP)'s performance by omitting the surrounding overhead introduced by the framework's processes. Each computation is executed three times with a one minute threshold on a freshly initialized REPL to counter inaccuracies in the measurements. The environment of this evaluation is a macOS 10.14.6 machine operating on a 7th generation i5 Intel processor at 3.1GHz. The displayed value representing a predicate's performance in milliseconds is obtained by averaging over the results of all three exemplary expressions, where every individual value is rounded half away from zero. The designation n.a. indicates that either a timeout or an \unsupported predicate exception" occurred. The benchmarks along with all performance measures for each run can be found on GitHub2.
The performance measurements of Figure 4 indicate that the native ProB, Kodkod and Z3 backend perform better compared to the s(CASP) backend, as their runtimes are generally faster. However, s(CASP) is able to obtain a result in some cases where Kodkod and Z3 are unable to follow. Furthermore, the plain s(CASP) engine's performances seem to be reasonable, as the corresponding runtimes are noticeably low in many cases. This suggests that the framework's overhead is considerably prevalent. On my machine I recorded an average startup time of 130 milliseconds for the Ciao engine. Compared to the best performing predicates the time of initialization renders roughly half of the entire process. However, these benchmarks are rather small compared to real-world examples. Hence, the time loss of the Ciao engine's initialization is more apparent.
In the following I express my thoughts on the gathered results. Note that these performances are heavily dependent on the e ciency of the custom predicates that are used for this translation, for instance member/2 or union/3. The predicates set comprehension, universal quanti er, cartesian product, cardinality, domain/range, composition, identity, domain/range restriction/subtraction, inverse, relational image, direct product, parallel product and function application share the fastest runtimes among this evaluation as they succeed in under 300 milliseconds. Cartesian product, cardinality, composition, identity, inverse, relational image, direct product, parallel product and function application merely iterate over a list without any demanding additional task along the way, which presumably leads to consuming less time. The predicates domain/range and domain/range restriction/subtraction make use of member/2 and set comprehension and universal quanti cation use s(CASP)'s built-in findall/3 predicate. I assume that these speci c benchmarks are not particularly challenging as further analysis suggests that the usage of member/2 and findall/3 leads to weaker performances.
Since s(CASP) lacks the cut operator, additional rules containing the goal not member/2 are needed to correctly express some predicate's behavior such as union/3 in this implementation. Consequently, in the instance of an element not being a member of the underlying list the rule invoking the negated goal is called nevertheless. This may induce further loss of time, especially for large lists. The other predicates, which mainly rely on member/2 are union, intersection, di erence, general union, general intersection and override. These predicates perform solidly relative to the aforementioned better performing ones.
The remaining predicates, i.e. powerset, relations, partial functions, total functions, partial injections, total injections, partial surjections, total surjections and bijections all invoke findall/3. These results show that the usage of findall/3 poses a considerable bottleneck for this framework's performance. The asterisk indicates that the benchmark's largest expression is not succeeding for the given threshold of one minute. For these particular benchmarks only the remaining two expressions are used including ProB. Considering the lacking e ciency the framework o ers a run option called \optimize", which lets ProB evaluate ground expressions before passing them to the framework. Predicate 4-Queens 5-Queens 6-Queens 7-Queens s(CASP) Plain s(CASP) 369 31 438 37 4927 3101 30507 5190
Figure 5 shows the performances of various ProB backends dealing with di erent sizes of the n-queens problem. Since this implementation seems to struggle with the computation of functions, these measurements are supported by ProB with the \optimize" feature enabled.
Overall, the s(CASP) backend's performance is not on par with the other ones. In particular, the s(CASP) backend is outclassed by the native ProB, Kodkod and Z3 backend in every single benchmark. Nevertheless, in some cases s(CASP) succeeds while Kodkod and Z3 are unable to solve the given constraint. Yet, even in those instances the native ProB backend poses a superior option. However, one needs to consider that this framework hardly incorporates any optimizations, i.e. predicates are straightforwardly translated in most cases. 6
Even though the presented framework is capable of translating a large portion of the B realm to s(CASP), there are some predicates left to be supported. Predicates such as iteration, closure, projection, lambda abstraction and the support of sequences should be included. Also enabling one to assign variables to in nite domains is imperative to be able to express more complex constraints. As s(CASP) o ers a CLP backend and shares similarities with Prolog, this probably could be done similarly to how ProB handles those instances. Furthermore, it is desirable to extend this framework so that the order of predicates in a conjunction is irrelevant. This could be done by analyzing the underlying AST within the framework, and thus generate appropriate code that is solely reliant on already evaluated predicates. Moreover, this work's evaluation indicates that improving the framework as a whole to reduce its surrounding overhead may lead to better performances. Reimplementing parts of the custom predicates that utilize findall/3 in a more e cient way should also lead to a more promising backend in general.
In conclusion, this work poses a foundation for translating B constraints to s(CASP). The empirical results indicate that the implemented backend is not quite on par with the other ones. However, I assume that this backend could be rendered more bene cial with further development. Furthermore, the presented backend can be used for veri cation of other employed solvers. Similar to how the s(CASP) backend is tested by ProB, ProB's and other solver's answers could thus be veri ed by s(CASP). Especially, for predicates that are solely supported by the native backend, the s(CASP) backend can be applied.