In today's class, we'll zoom out and think about some bigger questions around what Alloy can do.
Decidability
If you have taken CS235, you've heard about decidability.
A problem is decidable if there exists an algorithm to solve it that is always returns the correct answer and always terminates (that is, does not infinite loop).
We'll briefly relate this to what we've been doing so far in modeling with Alloy.
Let's start with this question:
For a given Alloy model, will a run or check statement always provide an answer, assuming enough computing resources and time?
Think, then click!
Yes, because of the finite scope! With a finite scope, check and run statements are decidable. Because the scope is finite, even a very inefficient implementation of the Alloy Analyzer could just enumerate all possible solutions to check if there is or is not a satisying instance to the model in question.
We'll come to see how Alloy's actual implementation is more efficient than this, but the "brute force" argument can be used to informally show decideability.
Even run/check statements for temporal models in Alloy, which reason over infinite traces, are deciable because Alloy is restricted to lasso traces–which have a finite number of states to analyze.
However, without the finite scope, Alloy models are not necessarily decidable! It is possible to formulate models in Alloy such that an analysis might potentially infinite loop in searching for a satisyfing instance, which makes the problem of model-finding undecidable.
The halting problem
The cannonical example of an undecidable problem is the halting problem. The formulation of the problem is this: can you write an algorithm that determines, for the source code of a program and an input to the program, whether the program will terminate (e.g., return) or run forever?
There is a classic proof (that we won't go over in CS340) that shows that the halting problem is undecideable, that is: no such algorithm exists. Many modeling tools that are not bounded run into there types of decidability issues.
Alloy is just one of a large number of modeling and formal methods tools. The assigned reading is a paper from Amazon about the investigations they took into applying Alloy, another tool called TLA+, and several other tools.
- The conclusion of this paper speaks to why this class is in Alloy: the author agrees that it is the easiest formal methods tool to pick up from scratch. The visual display in the Alloy Analyzer also makes it one of the most engaging ways to learn formal methods.
- The related course at Brown actually now uses a different, related tool called Forge that shares much of Alloy's syntax and semantics, but is not used in industry.
- One interesting point of the paper is that Alloy works better than expected on moderately complex concurrent problems, even before the temporal logic extension. With the additional of temporal logic, it would be interesting to reasses/recompare Alloy and TLA+ in this context.
Student question: the paper makes a distinction between direct and inductive modeling, what is the difference?
In direct modeling, you explicitly have sigs and atoms for every step in the trace you want to model. Lasso traces in a temporal Alloy model are an example of this.
In inductive modeling, you avoid explicitly modeling every step of a trace, and instead rely on inductive reasoning (similar to inductive proofs).
If we simplify the universe to good or bad states, the intuition for what an inductive model must show is:
- Every initial state is
good.
- Every possible transition from a
good state results in another good state.
Why do we not worry about transitions from bad states?
Think, then click!
We don't really care if a bad state transitions to another bad state, because in that trace we have already "lost". The initial state condition should ensure that if our system is correct, we never end up in a bad state to begin with.
Inductive models are less successful for reasoning about liveness properties (eventually, a specific good thing happens) because they typically only consider a single transition at a time.
Student question: the paper talks about the importance of the distributed mode of TLA+, what is that?
The distributed mode of TLA+ is about how the tool itself works, rather than specifically about what the user is trying to model.
As we'll see in the remainder of the semester, Alloy uses an underlying SAT solver. In 2014, most SAT solvers could not be run in a concurrent, distributed way.
TLA+ circa 2014, however, supported distrubuting its backend solving across multiple concurrent servers. This allowed analyzering/solving itself to finish faster for large problems.
In today's class, we'll zoom out and think about some bigger questions around what Alloy can do.
Decidability
If you have taken CS235, you've heard about decidability.
A problem is decidable if there exists an algorithm to solve it that is always returns the correct answer and always terminates (that is, does not infinite loop).
We'll briefly relate this to what we've been doing so far in modeling with Alloy.
Let's start with this question:
For a given Alloy model, will a
runorcheckstatement always provide an answer, assuming enough computing resources and time?Think, then click!
Yes, because of the finite scope! With a finite scope, check and run statements are decidable. Because the scope is finite, even a very inefficient implementation of the Alloy Analyzer could just enumerate all possible solutions to check if there is or is not a satisying instance to the model in question.
We'll come to see how Alloy's actual implementation is more efficient than this, but the "brute force" argument can be used to informally show decideability.
Even
run/checkstatements for temporal models in Alloy, which reason over infinite traces, are deciable because Alloy is restricted to lasso traces–which have a finite number of states to analyze.However, without the finite scope, Alloy models are not necessarily decidable! It is possible to formulate models in Alloy such that an analysis might potentially infinite loop in searching for a satisyfing instance, which makes the problem of model-finding undecidable.
The halting problem
The cannonical example of an undecidable problem is the halting problem. The formulation of the problem is this: can you write an algorithm that determines, for the source code of a program and an input to the program, whether the program will terminate (e.g., return) or run forever?
There is a classic proof (that we won't go over in CS340) that shows that the halting problem is undecideable, that is: no such algorithm exists. Many modeling tools that are not bounded run into there types of decidability issues.
Alternative modeling tools
Alloy is just one of a large number of modeling and formal methods tools. The assigned reading is a paper from Amazon about the investigations they took into applying Alloy, another tool called TLA+, and several other tools.
Discussion of Why Amazon Chose TLA+ paper, Newcombe
In direct modeling, you explicitly have sigs and atoms for every step in the trace you want to model. Lasso traces in a temporal Alloy model are an example of this.
In inductive modeling, you avoid explicitly modeling every step of a trace, and instead rely on inductive reasoning (similar to inductive proofs).
If we simplify the universe to
goodorbadstates, the intuition for what an inductive model must show is:good.goodstate results in anothergoodstate.Why do we not worry about transitions from
badstates?Think, then click!
We don't really care if a
badstate transitions to anotherbadstate, because in that trace we have already "lost". The initial state condition should ensure that if our system is correct, we never end up in abadstate to begin with.Inductive models are less successful for reasoning about liveness properties (eventually, a specific
goodthing happens) because they typically only consider a single transition at a time.The distributed mode of TLA+ is about how the tool itself works, rather than specifically about what the user is trying to model.
As we'll see in the remainder of the semester, Alloy uses an underlying SAT solver. In 2014, most SAT solvers could not be run in a concurrent, distributed way.
TLA+ circa 2014, however, supported distrubuting its backend solving across multiple concurrent servers. This allowed analyzering/solving itself to finish faster for large problems.