search

AlloyTools / org.alloytools.alloy

Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks. This repository contains the code for the tool.
Other
709 stars 124 forks source link

Add possibility to call SolveEngine to solve a model #51

Open AlexMSatalia opened 6 years ago

AlexMSatalia commented 6 years ago

I work for Satalia, which developped SolveEngine, an online Solver. I would like to contribute to Alloy in order to allow any user to solve their SAT models by calling SolveEngine.

aleksandarmilicevic commented 6 years ago

Sounds great. Can you create a pull request?

AlexMSatalia commented 6 years ago

Well first, I have to finish the code to commit, there are a few things that I cannot figure out how to do.

About that, would you know someone who could maybe give me some tips ? I sent an email to Ivan, who Satalia dealt with last year, but maybe he is not working anymore on the project, is he ?

Alex

On 3 May 2018 at 20:55, Aleksandar Milicevic notifications@github.com wrote:

Sounds great. Can you create a pull request?

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/AlloyTools/org.alloytools.alloy/issues/51#issuecomment-386416856, or mute the thread https://github.com/notifications/unsubscribe-auth/AbYXWm7meKCB1qsUFH48TDwIexfDL5gHks5tu2C7gaJpZM4Txlsc .

-- Alexandre MartinAlpha program intern | Lille, France +33 625806884 alexandre.martin@satalia. avida@satalia.comcom avida@satalia.com SATΛLIA http://satalia.com/

pkriens commented 6 years ago

On what level do you want to plug in? Currently we have

During the last workshop in Boston it looks like SMT is going to become extremely important. CVC4 is working on a relation theory and promised to have an Alloy solver. I think they plan to integrate on the Kodkod level.

I think the easiest way is to integrate on the CNF level for now. There are many examples, i.e. the SAT solvers we integrate. However, this interface is not completely clean and I plan to come up with a cleaner interface. Your effort could be a good way to start with this API.

AlexMSatalia commented 6 years ago

I think I plugged it in at the Alloy source code level. Just to be sure, here is a pull request I made on my personnal account so you could check the difference. I added the SolveEngine in the suggested solvers and added a new SATSolver.

https://github.com/alexandreMartinEcl/org.alloytools.alloy/pull/1

What I would like to do but am struggling a bit with are these:

Also, is the way I added the SolveEngine module to KodkodCore annoying or is it ok ?

If you know someone who could help me with that, it should me almost ready to merge

Alex

On 4 May 2018 at 08:02, Peter Kriens notifications@github.com wrote:

On what level do you want to plug in? Currently we have

  • The Alloy source code,
  • Alloy compiled AST,
  • Kodkod language,
  • Kodkod compiled AST (I think?),
  • CNF.

During the last workshop in Boston it looks like SMT is going to become extremely important. CVC4 is working on a relation theory and promised to have an Alloy solver. I think they plan to integrate on the Kodkod level.

I think the easiest way is to integrate on the CNF level for now. There are many examples, i.e. the SAT solvers we integrate. However, this interface is not completely clean and I plan to come up with a cleaner interface. Your effort could be a good way to start with this API.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/AlloyTools/org.alloytools.alloy/issues/51#issuecomment-386520244, or mute the thread https://github.com/notifications/unsubscribe-auth/AbYXWjIKcZa3NyQVksD90teU8E7Y1-hRks5tu_0egaJpZM4Txlsc .

-- Alexandre MartinAlpha program intern | Lille, France +33 625806884 alexandre.martin@satalia. avida@satalia.comcom avida@satalia.com SATΛLIA http://satalia.com/

pkriens commented 6 years ago

I am in a bit of a conundrum here. We need to make it easier to add solvers like yours, I do not think it should be necessary to change some of the core classes to add a solver as it is today, that is quite ugly and won't scale. I would prefer that you could add any solver by dropping a JAR in a directory somewhere. This then should have the possibility for that JAR to save private data.

However, this would require reworking some of the code, which will be a few days work. Since you seem to represent a commercial company, I'd ask the awkward question: Would you be willing to fund this? This work is on my todo list. However, it could be significantly expedited if I can treat it as commercial work. This would be very beneficial for the Alloytools project in general.

For the practical issues.

Don't worry about the stop button, the solver runs in its own process that is aborted by the Stop button. So you can catch the exit with a Runtime.shutdownHook and send the message to your backend to abort the job on your servers.

Dependencies are added in cnf/central.xml, which has the syntax of a Maven POM file. This makes the dependency available from a repository. You still then have to add it to the project in the bnd.bnd file in the -buildpath.

However ...

If you want to use JSON parser/coder then I do not like the idea to add some proprietary library to the core code like GSON. There is a decent standard for Java today, JSON-B, that will allow us to switch JSON libraries without killing a dependency like your proposal. (See http://json-b.net/)

Personally I am very excited about a commercial company that want to provide not this service. However, adding your service to Alloy means imho that we need to change Alloy so that you can add this service without changing any of the Alloy core code. The problem is that this requires work on the core Alloy code that needs to be funded by someone.

From my personal point of view I think we either change Alloy to make the solver really a separate plugin that is standalone and then accept your contribution. I am uncomfortable with adding your contribution on the same level as the open source SAT solvers.

Last. You currently plugin on the CNF level. CNF files can become HUGE. (Megabytes). These files will compress very badly with the popular compression algorithms since they consists of different integers. So you're looking at very long transfer times. It does seems the most straightforward way to plugin to Alloy today. However, we're looking very seriously at plugging in SMT solvers. Since these solvers provide different opportunities for integers, the plugin level will have to be higher than CNF. As far as I can see today, this is at the Kodkod level .

The Alloy AST is transformed to a Kodkod AST which is then translated to CNF. The Kodkod AST has similar size as the Alloy AST. You might want to consider to transfer the Kodkod AST to your backend since it does not explode while it contains all the decisions of Alloy and its options.

That said, I love the idea of a commercial backend ...

(These are personal views, Daniel and Aleks might have very different views since I am the newcomer here)