Logical puzzles can support teaching informatics and rational thinking. We have developed a metamodel-based approach supporting development, configuration, and automatic construction of puzzles with a syntax close to predicate logic and OCL and a semantics close to UML object models. (1) We extend this approach by introducing puzzle metrics expressed with OCL that consider puzzle complexity w.r.t. syntactic and semantic aspects. The aim of developing the metrics is to tune the logical puzzles for novice and expert players and learners. (2) Our UML and OCL model presents a new case study on the power and flexibility of OCL because OCL is here applied for various purposes and on diferent modeling levels.
In Fig. 1 our class model for representing logical puzzles is shown. Logical puzzles use clues and properties about imagined things that are to be described. Among the possible things, there is often one puzzle solution that is uniquely determined by the stated clues. A clue can ban things from being the solution. In our approach, the class model possesses a syntax part, classes Clue and Property, and a semantic part, the class Thing and the association between Clue and Thing with which a Clue is connected to a set of banned Thing objects, and a Thing is connected to a set of banning Clue objects. A central ingredient of the class model is the operation Thing::Valid(c:Clue) that computes whether a Clue evaluates to true or to false in a Thing. The class model can be understood best by discussing an object model that instantiates the classes. Figure 2 shows a puzzle with cards representing clues and a solution in progress indicated with tokens.
In our approach, clues take the form of an implication with a premise and a conclusion, both being a comparison between a property and a value Prop[=|<>]Val: PremProp[=|<>]PremVal => ConcProp[=|<>]ConcVal. Fig. 3 shows an example puzzle in which, roughly speaking, the two Property types top and bottom can take the three values red, green and blue as represented by the six Property objects. Two Clue objects are stated as implications: top<>blue => top=blue and body<>blue => top=green. This puzzle is automatically generated and will appear later in Fig. 4 in the first group of puzzles (with two clues) as Puz5. The nine Thing objects establish all puzzle solution candidates. The unique puzzle solution is the yellow marked Thing that is the only one where the attribute banned takes the value false. In the upper right, the (semantic) relationship between clues and things is pictured: A clue can ban a set of things, and things can be banned by a set of clues. The fact that T1 is the puzzle solution is reflected by the circumstance that T1 is not banned by any clue. Other links are not shown in the object diagram, however links can be deduced from the derived attributes toStr that are displayed in Clue and Thing objects.
All details of the model can be found in the Appendix. In particular all OCL expressions used as invariants, as operation definitions or as derivation rules for derived attributes or derived association ends can be found there. It is a rather compact, small model represented on basically only two pages. As central model features, we mention that (a) the operation Thing::valid(c:Clue) specifies whether a clue holds in a thing, and (b) the existence of a unique puzzle solution is formulated declaratively by the invariant oneThingWithCluesValidNotBanned.
Our metrics are divided into OCL expressions referring to the syntax part (referring to class Clue) and to the semantics part of the class model (referring to class Thing). The expressions about syntax count the number of occurrences of particular patterns in the clues; the expressions about semantics count clues, in which the things that are banned by the clue, possess particular properties. In more detail, we have developed the following seven metrics, i.e., OCL expressions. In the following we will partly refer to the metrics by their occurrence number in this list. E.g. metric 2 will refer to the expression about the number of ground facts.
Clue.allInstances->select(c|c.negatedP=true)->size+
Clue.allInstances->select(c|c.negatedC=true)->size 2. Number of ground facts
Clue.allInstances->
select(c|c.prem=c.conc and c.negatedP=true and c.negatedC=false)->size 3. Number of clues with diferent areas in premise and conclusion
Clue.allInstances->select(c|c.prem.name<>c.conc.name)->size 4. Number of clues banning nothing
Clue.allInstances->select(c|c.bannedT->isEmpty)->size 5. Number of clues banning exactly one thing
Clue.allInstances->select(c|c.bannedT->size=1)->size 6. Number of clues with equivalents
Clue.allInstances->select(c1|Clue.allInstances->exists(c2|
c1<>c2 and c1.bannedT=c2.bannedT))->size 7. Number of indispensable clues let C=Clue.allInstances in C->select(c1|c1.bannedT->exists(t|C->forAll(c2| c1<>c2 implies c2.bannedT->excludes(t))))->size
The first three metrics concentrate on the syntactic form of the clues and on its components, e.g. whether a clue contains a particular language feature. These metrics count: (1) the number of negations in the clues, (2) the number of clues representing de facto ground facts (i.e., whether the clue has the form not(A) implies A which is equivalent to not(not(A)) or A which again is equivalent to A or A and thus to A) and (3) the number of clues where premise and conclusion consider diferent property types. The last four metrics treat the semantics of clues and the connection between the clue and the set of banned Thing objects: (4) the number of clues without efect in the sense that the clue does not ban any possible Thing object, (5) the number of clues banning exactly one Thing object, (6) the number of clues possessing among all clues an equivalent diferent clue (banning the same set of Thing objects) and (7) the number of clues being indispensable in the sense that the clue bans a Thing object that is not banned by another clue. Typical metrics for software rely on the syntactic form of the underlying program text. In our approach we have explicitly modeled semantics through the class Thing and an appropriate association with class Clue, and thus we can take into account the efect, the semantics, that a clue has. We regard this as a unique feature of our approach that allows us to make well-argued statements about the complexity of a clue and with this whether a clue is well-suited for a novice or more suited for an expert.
We have validated that the metrics can be meaningfully applied with the running example introduced earlier. With the USE model validator we have generated 36 puzzles: 9 puzzles with 2 clues, 9 with 3 clues, 9 with 4 clues and 9 with 5 clues; the circumstance that we consider 9 puzzles comes from the fact that we have generated in each group all possible solutions for top and body color on the basis of 3 diferent colors ( 3 * 3 = 9). The table in Fig. 4 shows in each row a puzzle and in the columns the result of evaluating the metrics. Additionally, in the last column all metric values are summed up. As expected, with growing number of clues the puzzle complexity increases.
However, in each group with an equal number of clues, there are also diferences in the puzzle complexity between the various considered metrics. Let us discuss some details of the table. For example, in the 2-group (the puzzles with 2 clues) the metric 6 (Equivalents) must always evaluate to 0: if there are only 2 clues and the puzzle ofers only 2 properties ( top and body), there cannot be equivalent clues; similar arguments could be stated for metrics 4 (Banning Nothing) and 5 (Banning
One) since these metrics also evaluate to 0 in the 2-group. A further interesting point is that in the 5-group there is a wide range of use of negations (metric 1) ranging from clue sets with only 1 negation to clue sets with 9 negations. As the puzzles are automatically generated, there are also random decision taken by the USE model validator in the construction: E.g., in the 5-group, there are 2 puzzles with 2 equivalent clues, but there could also be 3 or 4 puzzles with that feature.
The metrics can even help to tune the syntactic representation of the clues, say, for novices or experts. If the metric on ground facts is non-zero, then there exists a clue in the form not(A) => A. For an expert, one could present the clue in this form; for a novice, one has the option to present the clue simply as A. In the running example, this would be, for example, a syntax representation like top<>red => top=red vs. a syntax representation like top=red.
The seven metrics that we have proposed are intended to demonstrate the options in our approach. A lot of further metrics on puzzle complexity could be formulated. For example, one could look for clue tuples in which the set of banned Thing objects of the first clue is strictly included in the set of banned Thing objects of the second clue. Or, one could look for clues that only ban Thing objects that are not banned by another clue.
OCL expressions are applied in our approach for diferent purposes and on diferent modeling levels (Fig. 5).
1. OCL expressions are part of the class model as class invariants (for syntax, semantics, and eficiency), operation definitions and derivation rules for derived attributes and association ends. 2. Clues may be thought of as class invariants in an imagined UML model representing the puzzle.
In the running example, one could think of the puzzle in terms of a class Car with attributes top:String, body:String and the invariants clue1: top<>’blue’ implies top=’blue’ and clue2: body<>’blue’ implies top=’green’. Finding an object model for this specification with fitting attribute values then corresponds to finding a solution for the logical puzzle. 3. When applying the Model Validator, we use classifying terms for generating many diverse object models each representing a puzzle solution. The classifying terms that we use are: SolutionTopColor let TC=Thing.allInstances->any(t | Clue.allInstances->
forAll(c | t.valid(c))).property->any(p|p.name=’top’).value in if TC=’red’ then 1 else if TC=’green’ then 2 else 3 endif endif SolutionBodyColor let BC=Thing.allInstances->any(t | Clue.allInstances->
forAll(c | t.valid(c))).property->any(p|p.name=’body’).value in if BC=’red’ then 1 else if BC=’green’ then 2 else 3 endif endif These two classifying terms take care that each two generated object models difer in at least one of the classifying terms. For a fixed number of clues, one obtains nine object models with diferent (top,body) color values from the range red, green, blue. 4. A further application of OCL lies in the main focus of our proposal, namely the use of OCL for formulating metrics that measure the puzzle complexity with regard to syntactic and semantic aspects.
OCL is applied in the original model in a declarative way. Furthermore, OCL is used in the sequential construction process together with the Model Validator in a way that guarantees that particular object models are found. And, in connection with the metrics, OCL is applied to optimize the user involvement and interaction.
For a full discussion of related work see [
Puzzles in education: The use of puzzles is a well-known approach to teaching of problem solving
skills and mathematical thinking [
Solving puzzles: The topic of solving puzzles has traditionally been addressed by using solvers of
diferent types (e.g., SAT or SMT solvers). For instance, in [
Developing puzzles: Some DSLs have been proposed to specify puzzles and their gaming context.
For instance, EGGG [
Figure 5: Applications of OCL in our approch.
The industry of logical puzzles: Although logical puzzles have a a tradition dating back many
centuries [
This contribution has refactored and extended an existing approach for the construction of logical puzzles. We have added various metrics for puzzles that allow to tune the puzzles, for example, for software novices or experts. The contribution has also highlighted the various options for application and use of OCL in the approach.
Future work to be done includes extending the form of clues that can be specified and polishing the existing implementation. On the side of the metrics, other options than the ones proposed here should be studied. In the polished implementation, the metrics should be incorporated automatically so that appropriate, diferent clues are presented, for example, to novices or experts.
Excellent reviewer remarks have improved the paper, although due to page limitations and our idea for paper structure we could not implement all. But we will respect the remarks in future work.
A. Class model including operation definitions, derivations and constraints (OCL elements only) class Thing attributes banned:Boolean toStr:Sequence(String) derive: self.property->iterate(p; r:Sequence(String)=Sequence{}| r->including(p.name+’ ’+p.value))->sortedBy(e|e) operations value(propertyP:String):String=
self.property->any(p|p.name=propertyP).value valid(c:Clue):Boolean = let pv:String=self.value(c.prem.name) in let pc:String=c.prem.value in let cv:String=self.value(c.conc.name) in let cc:String=c.conc.value in if c.negatedP=false and c.negatedC=false then (pv=pc implies cv=cc ) else if c.negatedP=false and c.negatedC=true then (pv=pc implies cv<>cc) else if c.negatedP=true and c.negatedC=false then (pv<>pc implies cv=cc ) else if c.negatedP=true and c.negatedC=true then (pv<>pc implies cv<>cc) else false endif endif endif endif bannedBy(c:Clue):Boolean = not(self.valid(c)) cluesValid():Set(Thing) =
Thing.allInstances->select(t |
Clue.allInstances->forAll(c | t.valid(c))) end association ClueConc between
Clue [0..*] role clueC
Property [1..1] role conc derive = Property.allInstances->any(p | self.conc=p) end association ClueThing between
Clue [0..*] role banningC Thing [0..*] role bannedT derive =
Thing.allInstances->select(t | t.bannedBy(self)) end class Clue attributes prem:Property negatedP:Boolean -- negated premise, e.g. *top<>blue* => bottom=red conc:Property negatedC:Boolean -- negated conclusion, e.g. bottom=red => *top<>blue* toStr:String derive: prem.name+if negatedP then ’<>’ else ’=’ endif+prem.value+’ => ’+ conc.name+if negatedC then ’<>’ else ’=’ endif+conc.value end constraints -- Constraints restricting syntactic elements context p1,p2:Property inv uniqueNameValue:
p1<>p2 implies (p1.name<>p2.name or p1.value<>p2.value) context t1,t2:Thing inv uniqueProperty:
t1<>t2 implies t1.property<>t2.property context t:Thing inv uniquePropertyName:
t.property->forAll(p1,p2 | p1<>p2 implies p1.name<>p2.name) context c1,c2:Clue inv uniqueClue: c1<>c2 implies ( c1.prem<>c2.prem or c1.conc<>c2.conc or
c1.negatedP<>c2.negatedP or c1.negatedC<>c2.negatedC ) -- Constraints restricting semantic elements context Thing inv thingsWithCluesValid_EQ_thingsNotBanned:
cluesValid()=Thing.allInstances->select(t | t.banned=false) context Thing inv oneThingWithCluesValidNotBanned:
cluesValid()->select(t | t.banned=false)->size=1 -- Constraints for Model Validator efficiency context t1,t2:Thing inv sameNumProperty:
t1.property->size=t2.property->size context p1,p2:Property inv sameNumThing:
p1.thing->size=p2.thing->size