Stack Overflow
Stack Overflow

Questions tagged [alloy]

Alloy from MIT is a declarative specification language for expressing complex structural constraints and behavior in a software system, and a tool for exploring and checking properties of the resulting structures.

Alloy from MIT is a declarative specification language for expressing complex structural constraints and behavior in a software system, and a tool for exploring and checking properties of the resulting structures.

The home page for Alloy is alloy.mit.edu.

Tutorials and documentation

  1. MIT Alloy tutorial page
  2. Official Alloy documentation

Reference books

  1. Software Abstraction by Daniel Jackson
594 questions
16
votes
3 answers

Experiences with using Alloy in real-world projects

I have been interested in formal methods for some time. I have used formal methods to reason about some very specific sub-areas of a few projects I have been working on. I was never able to convince other team members to try the same let alone…
VoidPointer
  • 17,651
  • 15
  • 54
  • 58
8
votes
5 answers

Have an object in one set or another, but not both?

This is homework and I'm having a lot of trouble with it. I am using Alloy to model a library. Here are the definitions of the objects: sig Library { patrons : set Person, on_shelves : set Book, } sig Book { authors : set Person, …
Ethan Mick
  • 9,517
  • 14
  • 58
  • 74
8
votes
0 answers

Running alloy analyzers in parallel

I am generating quite a lot of Alloys specifications (*.als files). For a medium-size problem I am trying to solve, I generated 1536 *.als files. In order to save time running all these files, I used the Java concurrency API (in particular…
bmorin
  • 645
  • 5
  • 12
5
votes
2 answers

Solving predicate calculus problems with Z3 SMT

I'd like to use Z3 to solve problems that are most naturally expressed in terms of atoms (symbols), sets, predicates, and first order logic. For example (in pseudocode): A = {a1, a2, a3, ...} # A is a set B = {b1, b2, b3...} C = {c1, c2,…
SRobertJames
  • 8,210
  • 14
  • 60
  • 107
5
votes
1 answer

Alloy's lone vs one quantifier on river crossing

In the river crossing Alloy model, this predicate: pred crossRiver [from, from', to, to': set Object] { one x: from | { from' = from - x - Farmer - from'.eats to' = to + x + Farmer } } models the river crossing: One of the objects x…
lynaghk
  • 63
  • 3
5
votes
1 answer

The best practice to use boolean in Alloy model

I'm building a simple Alloy to generate simple Java Pojo objects and some fields of that pojo are Boolean values. I'm now using the following mechanism to achieve this function one sig item { autoPay: String, Price: Int } fact boolean { …
user2744486
  • 161
  • 1
  • 3
  • 10
5
votes
1 answer

Alloy built-in integer math functions don't work in imported files

I have an alloy model in avlTree.als. This model uses integer arithmetic, specifically the plus and minus functions. This model has some assertions in it, and I can run those just fine using the Alloy Analyzer GUI. I have another alloy model in…
SethQ
  • 53
  • 3
5
votes
2 answers

Meaning of 'private' keyword in Alloy? Meaning of 'enum' declaration?

The Alloy 4 grammar allows signature declarations (and some other things) to carry a private keyword. It also allows Allow specifications to contain enumeration declarations of the form enum nephews { hughie, louis, dewey } enum ducks { donald,…
C. M. Sperberg-McQueen
  • 24,596
  • 5
  • 38
  • 65
4
votes
1 answer

How to use Alloy to find faults in software architecture

I'm having lots of fun learning Alloy, and am excited to apply it to some software projects I am working on. In the past, I've used lightweight formal methods informally, if it were, to write in first order logic some of the invariants that I expect…
SRobertJames
  • 8,210
  • 14
  • 60
  • 107
4
votes
1 answer

understanding the 'this' keyword in Alloy

In the following code from section 4.7.2 of the Alloy book, what does the this keyword refer to? module library/list [t] sig List {} sig NonEmptyList extends List {next: List, element: t} ... fun List.first : t {this.element} fun List.rest : List…
qartal
  • 2,024
  • 19
  • 31
4
votes
1 answer

Univ signature appears magically when module is empty

I have in front of me an Alloy model composed of different modules (files). The main module (the one containing the command) does not contain any signature declaration, only a command and some facts. This model enforces that only one instance can…
Loïc Gammaitoni
  • 4,173
  • 16
  • 39
4
votes
1 answer

Alloy: facts etc. about Int

i am recently working with Alloy. Can I say something like: fact{ all i: Int | i >= 0 } I want to say: all Integer which Alloy uses should be positive. Alloy doesn't fail but also don't give me instances. greetings
Lao Tse
  • 171
  • 3
  • 12
4
votes
1 answer

Alloy - Generate .xml instance from .als

I need to generate random .xml instances from an .als in my program. I managed to do that by running alloy in background (invisible JFrame) and calling the doOpen, doExecuteLatest and doShowLatest functions. But having to wait alloy to start every…
mcopo
  • 103
  • 1
  • 6
4
votes
1 answer

going through an A4Solution

I am currently using the Alloy api in my project, and I need to display A4Solutions.I can do that easily with the vizualiser Alloy provides (vizGUI) , but it is a bit too limited for my purpose. So I am willing to generate my own graphs ( using any…
Loïc Gammaitoni
  • 4,173
  • 16
  • 39
4
votes
1 answer

semantic change in 4.2?

My question is whether the semantics of () in the declaration of fields had changed in Alloy 4.2. I read in "Software Abstractions" that addr: (Book -> Name) -> lone Addr means that the relation addr associates at most one address with each…
user2017729
  • 41
  • 1
1
2 3
…
39 40