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
696 stars 124 forks source link

Add model counting function to Alloy #127

Closed jiayiyang1997 closed 2 years ago

jiayiyang1997 commented 3 years ago

Dear Alloy community,

I'm Jiayi Yang, a graduate student from UT Austin. Our research group is integrating a new function (model counting function) to Alloy, which includes adding support for two state-of-art model counters (ApproxMC: https://github.com/meelgroup/ApproxMC & ProjMC: http://www.cril.univ-artois.fr/kc/projmc.html) and extending the grammar of expect clauses to better satisfy users' requirements. The detailed introduction and demo can be found here: https://github.com/jiayiyang1997/org.alloytools.alloy/tree/model_count.

This work is accepted by ESEC/FSE 2020 - Tool Demonstrations (not published yet). We plan to submit a pull request for this work and hope to make Alloy an even stronger tool-set which is specifically helpful in scenarios where the approximate number of possible solutions to a formula is desired. We'd appreciate any feedback you may have.

Thanks, Jiayi

pkriens commented 2 years ago

See PR, should make a more formal proposal.