5 ms·

Alloy*: A Higher-Order Relational Constraint Solver

201 points by Cieplak 8y ago

sidereal 8y ago
Before learning about Alloy*, you might want to learn about Alloy itself: http://alloy.lcs.mit.edu/alloy/index.html http://alloy.lcs.mit.edu/alloy/index.html Hillel Wayne has a great series of blog posts on using Alloy to solve software design problems: https://www.hillelwayne.com/tags/alloy/ https://www.hillelwayne.com/tags/alloy/
- yesenadam 8y ago
  (I'm no expert but..) I recently got into Prolog, and Alloy sounds very similar. So I was asking "How is it different?" Strangely, in the FAQ, no mention of Prolog. I found just this: >How does the Alloy Analyzer differ from theorem provers? >The Alloy Analyzer's analysis is fully automatic, and when an assertion is found to be false, the Alloy Analyzer generates a counterexample. It's a "refuter" rather than a "prover". (i.e. where Prolog would just write "no" if nothing found.) In the Alloy* paper also, no mention of Prolog. To find a counterexample, couldn't you set Prolog to find one?
  - Jtsummers 8y ago
    You could try in Prolog. But the other difference is that prolog is. General purpose language (though used in a more specific set of situations). Alloy is not. Also the search mechanisms are not the same. Prolog uses a backtracking, depth-first search behind the scenes. Alloy does not. EDIT: I was out earlier and didn't want to make a claim I couldn't verify/backup. Alloy uses a SAT solver behind the scenes to find solutions.
  - sriram_malhar 8y ago
    Alloy is a specification language. To verify the specification, the alloy analyser (a model checker) has to artificially create some number of instances and simulate it. Prolog is an executable language. You, the user, give it a database, and it searches for solutions that satisfies constraints. It doesn't create the basic facts on its own. There exists a compiler from imperative alloy to prolog to make this transition.
    - yesenadam 8y ago
      Hmm well, not all Prolog uses fit the 'give it a database' model..(In fact I can't think of any Prolog programs I've seen that do fit it) e.g. I was tried the the finite domain solver in Gnu Prolog[0] recently, I wanted arrangements of about 15 shapes that obeyed certain constraints, the program was 6 very short lines! I didn't tell it anything except the constraints. But yeah, alloy and alloy* sound fascinating, I must investigate further, thank you. [0]http://www.gprolog.org/manual/html_node/gprolog054.html http://www.gprolog.org/manual/html_node/gprolog054.html
      - sriram_malhar 8y ago
        You are right. Constraint solving in general is a specific area that does not require a knowledge base; instead it is a search for a solution from the specified domain that fits all the specified constraints. Here there is considerable overlap between prolog, alloy and z3. However, most general prolog programming has the same requirements placed on other executable languages, to transform, store and communicate data. Alloy is not the tool for this aspect.
  - Cieplak 8y ago
    Was recently asking the exact same question, and this is the best answer I found regarding some of the limitations of Prolog: https://faculty.nps.edu/ncrowe/book/chap14.html https://faculty.nps.edu/ncrowe/book/chap14.html
  - AnaniasAnanas 8y ago
    Prolog is Turing-complete, you can have non-terminating programs in it (and thus there are problems that can be expressed in Prolog that you can never get an answer to), does the same hold true for Alloy? If not I think that it would make more sense to compare Datalog (which I think forces all of its programs to provably terminate) with Alloy rather than Prolog with Alloy.
    - hwayne 8y ago
      Alloy forces you to bound all of your models, so it will always terminate.
  - fspeech 8y ago
    Prolog is a general programming language with built-in backchaining semantics. It in general does not know how to solve constraints. Indeed if your clauses have loops Prolog will just run in circles until it is out of stack space. The following common rules for equivalence are good examples of valid logic statements that do not work with Prolog's naive execution strategy: % Symmetry f(A, B) :- f(B, A). % Transitivity f(A, C) :- f(A, B), f(B, C). Indeed in general finding the symmetric/transitive closure of relations is a very hard problem. Constraint/SAT solvers use heuristics to solve problems like the above and can accept much more declarative specifications than Prolog.
bayesian_horse 8y ago
Sometimes it would be great for such posts to somehow explain to the uninitiated why you want to be initiated. "Relational Constraint Solver" sounds sort of interesting, but I haven't the faintest clue what I could use it for, and that's not that common for me.
- fspeech 8y ago
  Alloy (and the philosophy it is based on) is explained in Daniel Jackson's book <<Software Abstractions>>, which is a very nice book to read on techniques of specification and verification (at the specification level).
  - bayesian_horse 8y ago
    I got that. What exactly is exciting about such verification, especially despite the theoretical complexity, effort, and lack of common use? I really don't want to insult anyone with these questions. I'm genuinely curious why people spend time on such things and presuppose there are good reasons. I just don't know them yet.
- kilburn 8y ago
  Disclaimer: I'm not an expert so anything down here may be wrong. The "most basic" form of solver in this world is a SAT solver: it takes a logic formula of conjunctions and disjunctions (ANDs and/or ORs), defined over binary variables, and either finds an assignment to the variables that satisfies it or states that there is no such assignment (the formula cannot be satisfied). From this simple case, you can expand in several directions: a) Accept first order logic formulas (adds "forall" ∀, "exists" ∃, and "implication" → to the formulas). b) Accept formulas with variables of other types/(theories), such as integers, floats, sets. These are known as satisfiability modulo theories (SMT) solvers. c) Accept relational algebra operators (projection, selection, join, etc.) d) ... anything you can think of that makes solving your particular problem more efficient. All of these extensions can be "translated" to a SAT problem/formula. The issue is that the translated formula often grows exponentially (i.e.: add one variable to an SMT formula, and you get "times n" variables in the SAT translation). The advantage of these "specialized" forms of solvers is twofold: 1) They receive better semantical information about the problem, and hence can use more compact representations and optimization tricks that the non-specialized solvers cannot use. 2) They make it easier for users to specify their problems (this could be solved by an automated translator though). Now that we have a way to reason about what different constraint solvers are and how they relate to each other, we can translate "Alloy* : A Higher-Order Relational Constraint Solver" to "a constraint solver that exploits relational operators and higher-order constraints". "First order" is ∃, ∀, etc. above, "Higher order" is ∀∃, ∃∀, etc. treated as a semantically distinct case that allows for better optimizations. Of course, these specializations are (usually) not done just because they are fun to do. They are developed as ongoing efforts to use constraint solving techniques to solve actual problems. In this case they highlight Alloy* as a solver for: - Optimization problems (meeting scheduling, planning, etc.) - Model checking / program verification. - Program generation.
_pmf_ 8y ago
What would be really great if Alloy (or any spec language) allowed for code generation (even if inefficient code).
rurban 8y ago
I still find cbmc easier to find exhaustive counterexamples or test cases, because I can do it in straight C. With ATS or spark/Ada I can also do the same, but much more. I can actually solve the problem, not only prove that it is solvable or incorrect.

201 points by Cieplak 8y ago

Before learning about Alloy*, you might want to learn about Alloy itself: http://alloy.lcs.mit.edu/alloy/index.html http://alloy.lcs.mit.edu/alloy/index.html Hillel Wayne has a great series of blog posts on using Alloy to solve software design problems: https://www.hillelwayne.com/tags/alloy/ https://www.hillelwayne.com/tags/alloy/

yesenadam 8y ago
(I'm no expert but..) I recently got into Prolog, and Alloy sounds very similar. So I was asking "How is it different?" Strangely, in the FAQ, no mention of Prolog. I found just this: >How does the Alloy Analyzer differ from theorem provers? >The Alloy Analyzer's analysis is fully automatic, and when an assertion is found to be false, the Alloy Analyzer generates a counterexample. It's a "refuter" rather than a "prover". (i.e. where Prolog would just write "no" if nothing found.) In the Alloy* paper also, no mention of Prolog. To find a counterexample, couldn't you set Prolog to find one?
- Jtsummers 8y ago
  You could try in Prolog. But the other difference is that prolog is. General purpose language (though used in a more specific set of situations). Alloy is not. Also the search mechanisms are not the same. Prolog uses a backtracking, depth-first search behind the scenes. Alloy does not. EDIT: I was out earlier and didn't want to make a claim I couldn't verify/backup. Alloy uses a SAT solver behind the scenes to find solutions.
- sriram_malhar 8y ago
  Alloy is a specification language. To verify the specification, the alloy analyser (a model checker) has to artificially create some number of instances and simulate it. Prolog is an executable language. You, the user, give it a database, and it searches for solutions that satisfies constraints. It doesn't create the basic facts on its own. There exists a compiler from imperative alloy to prolog to make this transition.
  - yesenadam 8y ago
    Hmm well, not all Prolog uses fit the 'give it a database' model..(In fact I can't think of any Prolog programs I've seen that do fit it) e.g. I was tried the the finite domain solver in Gnu Prolog[0] recently, I wanted arrangements of about 15 shapes that obeyed certain constraints, the program was 6 very short lines! I didn't tell it anything except the constraints. But yeah, alloy and alloy* sound fascinating, I must investigate further, thank you. [0]http://www.gprolog.org/manual/html_node/gprolog054.html http://www.gprolog.org/manual/html_node/gprolog054.html
    - sriram_malhar 8y ago
      You are right. Constraint solving in general is a specific area that does not require a knowledge base; instead it is a search for a solution from the specified domain that fits all the specified constraints. Here there is considerable overlap between prolog, alloy and z3. However, most general prolog programming has the same requirements placed on other executable languages, to transform, store and communicate data. Alloy is not the tool for this aspect.
- Cieplak 8y ago
  Was recently asking the exact same question, and this is the best answer I found regarding some of the limitations of Prolog: https://faculty.nps.edu/ncrowe/book/chap14.html https://faculty.nps.edu/ncrowe/book/chap14.html
- AnaniasAnanas 8y ago
  Prolog is Turing-complete, you can have non-terminating programs in it (and thus there are problems that can be expressed in Prolog that you can never get an answer to), does the same hold true for Alloy? If not I think that it would make more sense to compare Datalog (which I think forces all of its programs to provably terminate) with Alloy rather than Prolog with Alloy.
  - hwayne 8y ago
    Alloy forces you to bound all of your models, so it will always terminate.
- fspeech 8y ago
  Prolog is a general programming language with built-in backchaining semantics. It in general does not know how to solve constraints. Indeed if your clauses have loops Prolog will just run in circles until it is out of stack space. The following common rules for equivalence are good examples of valid logic statements that do not work with Prolog's naive execution strategy: % Symmetry f(A, B) :- f(B, A). % Transitivity f(A, C) :- f(A, B), f(B, C). Indeed in general finding the symmetric/transitive closure of relations is a very hard problem. Constraint/SAT solvers use heuristics to solve problems like the above and can accept much more declarative specifications than Prolog.

bayesian_horse 8y ago

Sometimes it would be great for such posts to somehow explain to the uninitiated why you want to be initiated. "Relational Constraint Solver" sounds sort of interesting, but I haven't the faintest clue what I could use it for, and that's not that common for me.

fspeech 8y ago
Alloy (and the philosophy it is based on) is explained in Daniel Jackson's book <<Software Abstractions>>, which is a very nice book to read on techniques of specification and verification (at the specification level).
- bayesian_horse 8y ago
  I got that. What exactly is exciting about such verification, especially despite the theoretical complexity, effort, and lack of common use? I really don't want to insult anyone with these questions. I'm genuinely curious why people spend time on such things and presuppose there are good reasons. I just don't know them yet.
kilburn 8y ago
Disclaimer: I'm not an expert so anything down here may be wrong. The "most basic" form of solver in this world is a SAT solver: it takes a logic formula of conjunctions and disjunctions (ANDs and/or ORs), defined over binary variables, and either finds an assignment to the variables that satisfies it or states that there is no such assignment (the formula cannot be satisfied). From this simple case, you can expand in several directions: a) Accept first order logic formulas (adds "forall" ∀, "exists" ∃, and "implication" → to the formulas). b) Accept formulas with variables of other types/(theories), such as integers, floats, sets. These are known as satisfiability modulo theories (SMT) solvers. c) Accept relational algebra operators (projection, selection, join, etc.) d) ... anything you can think of that makes solving your particular problem more efficient. All of these extensions can be "translated" to a SAT problem/formula. The issue is that the translated formula often grows exponentially (i.e.: add one variable to an SMT formula, and you get "times n" variables in the SAT translation). The advantage of these "specialized" forms of solvers is twofold: 1) They receive better semantical information about the problem, and hence can use more compact representations and optimization tricks that the non-specialized solvers cannot use. 2) They make it easier for users to specify their problems (this could be solved by an automated translator though). Now that we have a way to reason about what different constraint solvers are and how they relate to each other, we can translate "Alloy* : A Higher-Order Relational Constraint Solver" to "a constraint solver that exploits relational operators and higher-order constraints". "First order" is ∃, ∀, etc. above, "Higher order" is ∀∃, ∃∀, etc. treated as a semantically distinct case that allows for better optimizations. Of course, these specializations are (usually) not done just because they are fun to do. They are developed as ongoing efforts to use constraint solving techniques to solve actual problems. In this case they highlight Alloy* as a solver for: - Optimization problems (meeting scheduling, planning, etc.) - Model checking / program verification. - Program generation.

_pmf_ 8y ago

What would be really great if Alloy (or any spec language) allowed for code generation (even if inefficient code).

rurban 8y ago

I still find cbmc easier to find exhaustive counterexamples or test cases, because I can do it in straight C. With ATS or spark/Ada I can also do the same, but much more. I can actually solve the problem, not only prove that it is solvable or incorrect.