Improve REPL Interaction

[thedotmatrix]

Break up functionality into several context "modes": Theory Mode Incomplete Model Mode? Vertical Exploration / Augmentation Stack Horizontal Exploration / Model Stream Queue Explanation / Provenance Queries

Also, make sure the context "where the user is in Razor after each command" is better communicated to the user. Emphasize that Razor is a Model Assistant!

[salmans]

This is how I think about exploring the space of all models: theoretically speaking, in every run of Razor, the user should be able to explore all models of the theory at least once. However, once the user leaves a model, s/he may have to rerun Razor to visit the model again. This is consistent with how most model-finders (including Alloy and Paradox) present the models to the user; i.e., a one way iterator that only goes forward. Due to augmentation, the space of models in Razor has two dimensions whereas conventional model-finders provide a one-dimensional iterator.

So, I think it is reasonable to think about the stream of models at every level (i.e., no augmentation) as a unidirectional iterator with "next" but not "previous". This won't require any extra work in the core of Razor. However, we need to support backtracking after augmentation so that the user can continue exploring the space of models and visit the remaining models of the theory at least once:

1. The REPL has to maintain a stack of possible fact bases and provenance information. With every augmentation, a new (base, prov) pair is pushed into the stack and with every backtrack (from augmentation) the previous item is popped.
2. The state of computation for the set of ground sequents can be maintained using the SMT solver's push and pop operations. Therefore, Razor's SAT module has to provide the REPL with push and pop, which directly map to the solver's push and pop operations.

@ryandanas, if you agree with my proposal, I can go ahead and implement the push and pop functions in SAT.

[dandougherty]

Let me raise a question. Is it significantly harder to implement horizontal backtracking then vertical backtracking? Since: I don't buy the conceptual distinction: if I am a user I can imagine just as well going back horizontally as vertically.

If it is much harder to do horizontal than vertical then that is an OK reason to do one and not the other. But I do not buy the reasoning, "This is consistent with how most model-finders (including Alloy and Paradox) present the models to the user; i.e., a one way iterator that only goes forward..."

We are building a "model-finding assistant* right? Let's be better than they are.

Dan

On Wed, Nov 26, 2014 at 2:11 PM, Salman Saghafi notifications@github.com wrote:

This is how I think about exploring the space of all models: theoretically speaking, in every run of Razor, the user should be able to explore all models of the theory at least once. However, once the user leaves a model, s/he may have to rerun Razor to visit the model again. This is consistent with how most model-finders (including Alloy and Paradox) present the models to the user; i.e., a one way iterator that only goes forward. Due to augmentation, the space of models in Razor has two dimensions whereas conventional model-finders provide a one-dimensional iterator.

So, I think it is reasonable to think about the stream of models at every level (i.e., no augmentation) as a unidirectional iterator with "next" but not "previous". This won't require any extra work in the core of Razor. However, we need to support backtracking after augmentation so that the user can continue exploring the space of models and visit the remaining models of the theory at least once:

1. The REPL has to maintain a stack of possible fact bases and provenance information. With every augmentation, a new (base, prov) pair is pushed into the stack and with every backtrack (from augmentation) the previous item is popped.
2. The state of computation for the set of ground sequents can be maintained using the SMT solver's push and pop operations. Therefore, Razor's SAT module has to provide the REPL with push and pop, which directly map to the solver's push and pop operations.

@ryandanas https://github.com/ryandanas, if you agree with my proposal, I can go ahead and implement the push and pop functions in SAT.

Reply to this email directly or view it on GitHub https://github.com/salmans/Razor/issues/35#issuecomment-64696188.

[salmans]

Before I argue that horizontal backtracking might be theoretically impossible, my short answer is that horizontal backtracking needs a more complicated notion of state at least. I am guessing that we don't have enough time to come up with a stable implementation in the remaining time until our first release on Dec 1. So, if my argument below is incorrect, I suggest to leave horizontal backtracking for the next release.

Having said that, I think horizontal backtracking is impossible theoretically. Notice that:

1. The tool for getting the next model from the solver is to extend the input theory with additional clauses that forces the solver to return a model that is not the same as any of the previous models.
2. Our tool for implementing backtracking is to use the solver's internal stack, which allows us to extend the input with additional clauses (using push) and remove the last set of pushed clauses (using pop) and return the solver to its previous state, before adding the last set of clauses.

But here is the problem: the solver's behavior is not deterministic (although for small inputs they tend to show a deterministic behavior). When we vertically backtrack, the solver only guarantees that we land on the previous iterator of models but not necessarily the model that was augmented. So, the user shouldn't think about backtracking as a way to get back to the previous model, rather as a way to undo the augmentation. However, horizontal backtracking only makes sense if we actually return to the previous model (as opposed to allowing the solver to return the previous model), but the solver doesn't guarantee the previous model after undoing the last set of changes.

[dandougherty]

ok, sure, I accept this argument, that it is difficult to implement (too difficult for this release)

For the longer term, this remark seems to be strong: " I think horizontal backtracking is impossible theoretically..." In the worst case we could just save the models, right? Even write all the associated state to a file if we had to. I'm not offering that as a good solution, but the goal is not impossible

Dan

On Wed, Nov 26, 2014 at 3:54 PM, Salman Saghafi notifications@github.com wrote:

Before I argue that horizontal backtracking might be theoretically impossible, my short answer is that horizontal backtracking needs a more complicated notion of state at least. I am guessing that we don't have enough time to come up with a stable implementation in the remaining time until our first release on Dec 1. So, if my argument below is incorrect, I suggest to leave horizontal backtracking for the next release.

Having said that, I think horizontal backtracking is impossible theoretically. Notice that:

1. The tool for getting the next model from the solver is to extend the input theory with additional clauses that forces the solver to return a model that is not the same as any of the previous models.
2. Our tool for implementing backtracking is to use the solver's internal stack, which allows us to extend the input with additional clauses (using push) and remove the last set of pushed clauses (using pop) and return the solver to its previous state, before adding the last set of clauses.

But here is the problem: the solver's behavior is not deterministic (although for small inputs they tend to show a deterministic behavior). When we vertically backtrack, the solver only guarantees that we land on the previous iterator of models but not necessarily the model that was augmented. So, the user shouldn't think about backtracking as a way to get back to the previous model, rather as a way to undo the augmentation. However, horizontal backtracking only makes sense if we actually return to the previous model (as opposed to allowing the solver to return the previous model), but the solver doesn't guarantee the previous model after undoing the last set of changes.

Reply to this email directly or view it on GitHub https://github.com/salmans/Razor/issues/35#issuecomment-64709223.

[salmans]

Sure! I agree that impossible is too strong but even in the case of storing all models, it is not clear to me how we can recover the solver's previous states.

[dandougherty]

PS. Granted that we will not implement horizontal backtracking, let's talk about it (in person and in documentation) as a feature that is not yet implemented, as opposed to talking about it as a different kind of movement in the model-space. One of things we are doing here is introducing our users to a certain conceptual framework for thinking about the models ----remember that, although we have a mental model of things, most users won't have a picture of the space of models as having any structure...the perceived benefit of Razor depends on people buying into that conceptual model.

On Wed, Nov 26, 2014 at 3:54 PM, Salman Saghafi notifications@github.com wrote:

Before I argue that horizontal backtracking might be theoretically impossible, my short answer is that horizontal backtracking needs a more complicated notion of state at least. I am guessing that we don't have enough time to come up with a stable implementation in the remaining time until our first release on Dec 1. So, if my argument below is incorrect, I suggest to leave horizontal backtracking for the next release.

Having said that, I think horizontal backtracking is impossible theoretically. Notice that:

1. The tool for getting the next model from the solver is to extend the input theory with additional clauses that forces the solver to return a model that is not the same as any of the previous models.
2. Our tool for implementing backtracking is to use the solver's internal stack, which allows us to extend the input with additional clauses (using push) and remove the last set of pushed clauses (using pop) and return the solver to its previous state, before adding the last set of clauses.

But here is the problem: the solver's behavior is not deterministic (although for small inputs they tend to show a deterministic behavior). When we vertically backtrack, the solver only guarantees that we land on the previous iterator of models but not necessarily the model that was augmented. So, the user shouldn't think about backtracking as a way to get back to the previous model, rather as a way to undo the augmentation. However, horizontal backtracking only makes sense if we actually return to the previous model (as opposed to allowing the solver to return the previous model), but the solver doesn't guarantee the previous model after undoing the last set of changes.

Reply to this email directly or view it on GitHub https://github.com/salmans/Razor/issues/35#issuecomment-64709223.

[thedotmatrix]

Apologies for the delayed reply. @salmans I agree with your first message, and if you have the time to implement that, it would be great. If not I can do it as soon as I get the repl-modes set up. And, looking at the rest of the comments, I agree that it's something that will require some additional thought, but is a feature we would like to have sometime after this release.

[salmans]

OK, I just added two functions, satPush and satPop, to the interface of SAT solving modules. I'm guessing these functions are enough for implementing our ideas for the REPL. Please let me know if anything is missing or if the functions don't behave as they're supposed to. I haven't tested the functions!

[thedotmatrix]

The new REPL is mostly complete. I would like to discuss it and get some feedback before merging it into the Razor branch.

[thedotmatrix]

Current TODO before push to Razor branch...

Transition to query mode should show model query help: origins show all the origins of the representatives Add copyright to splash. Add copyrights to files in REPL folder / put LANGUAGE under header Rename the GStar type to ChaseState; GStar is a misnomer Only have one mode for EXPLOREation Add Augmentation Stack to the overall Razor state; make sure push/pop work; make sure the stack carries over to other modes.

Future Ideas:

Do something similar to / use John's PrettyPrinting monad / class? Verbose / Debug printouts for the REPL?

[thedotmatrix]

Everything is taken care of other than the modelspace / exploration / augmentation bugs. Updates for that will go into a separate issue. This issue will be closed when my branch is merged / pushed into the razor branch.