Below is an Alloy model that type checks and works as expected in the last stable release but fails to type check in the latest build.

This seems to be a bug in the type checker ...

module list 		 

one sig Null {}		 

sig Str {}				

sig Node {
  data: one Str + Null,	 
  next: one Node + Null	 
}

sig List {
  head: one Node + Null	 
}

one sig This extends List {}

pred Inv[next: Node->(Node + Null) ] {
  no ^next & iden
}

pred Pre[This: List, head:  List->(Node + Null), next: Node->(Node + Null)] {
  This.head != Null &&
  This.head.next != Null
}

pred Post[This: List, oldHead, head:  List->(Node + Null), oldNext, next: Node->(Node + Null)] {
  This.head.*next = This.oldHead.*oldNext && 
  let N = This.oldHead.*oldNext - Null |
   next = oldNext ++ ~(oldNext & N->N) ++
               This.oldHead->Null
                
}

fun near0[] : Node+Null { This.head }
fun mid0[] : Node+Null { near0.next }
fun far0[] : Node+Null { mid0.next }

fun next0[] : Node->(Node + Null) { next ++ (near0 -> far0) }
pred guard[] { far0 != Null }
fun next1[] : Node->(Node + Null) { next0 ++ (mid0 -> near0) }
fun near1[] : Node+Null { mid0 }
fun mid1[] : Node+Null { far0 }
fun far1[] : Node+Null { far0.next1 }

fun near2[] : Node+Null { guard => near1 else near0 }
fun mid2[] : Node+Null { guard => mid1 else mid0 }
fun far2[] : Node+Null { guard => far1 else far0 }

fun next2[] : Node->(Node + Null) { guard => next1 else next0 }
fun next3[] : Node->(Node + Null) { next2 ++ (mid2 -> near2) }
fun head0[] : List->(Node + Null)  { head ++ (This -> mid2) }

run {
  far2 = Null &&
  Inv[next] && 
  Pre[This, head, next] &&
  !(Inv[next3] && Post[This, head, head0, next, next3])
} for 1 List, 3 Node, 3 Str, 1 Null

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.

The "add" function in the following simple model doesn't work consistently if it's chained (see assertion "addWorksFluently") but works fine without chaining (see assertion "addWorks")

sig IntSet{
   values: set Int
}

fun IntSet.add(value: Int): IntSet {
   { result: one IntSet | result.values = this.values + value }
}

fun emptySet: IntSet {
   { result: IntSet | no result.values }
}

assert emptySetWorks{
   all myIntSet: IntSet |
      myIntSet = emptySet implies no myIntSet.values and myIntSet.values = none
}
check emptySetWorks

assert addWorks {
   all disj s1, s2: IntSet |
      s1 = emptySet.add[0] and
      s2 = s1.add[1]
      implies
      s1.values = 0 and
      s2.values = 0 + 1
}
check addWorks

assert addWorksFluently {
   all disj s: IntSet |
      s = emptySet.add[0].add[1]
      implies
      s.values = 0 + 1
}
check addWorksFluently

I tried to run Alloy 4.2 and Alloy 5.0beta 4 on my Mac with High Sierra and Java 9.

I get the following exception:

Exception: class java.lang.NoSuchMethodError Message: java.lang.NoSuchMethodError: com.apple.eawt.Application.addPreferencesMenuItem()V Stacktrace: class java.lang.NoSuchMethodError: com.apple.eawt.Application.addPreferencesMenuItem()V edu.mit.csail.sdg.alloy4whole.SimpleGUI.<init>(SimpleGUI.java:1546) edu.mit.csail.sdg.alloy4whole.SimpleGUI.<init>(SimpleGUI.java:179) edu.mit.csail.sdg.alloy4whole.SimpleGUI$7.run(SimpleGUI.java:1519) java.desktop/java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:313) java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:764) java.desktop/java.awt.EventQueue.access$500(EventQueue.java:97) java.desktop/java.awt.EventQueue$3.run(EventQueue.java:717) java.desktop/java.awt.EventQueue$3.run(EventQueue.java:711) java.base/java.security.AccessController.doPrivileged(Native Method) java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:89) java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:734) java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:199) java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124) java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113) java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109) java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101) java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)

I have been using Alloy 4.2 on that Mac for 4 years without problem with previous versions of the OS and Java JVM.

Currently, the said commands (CTRL+LEFT, CTRL+RIGHT, CTRL+BACKSPACE, CTRL+DELETE) do not jump over/delete the Alloy sentences as they should (for instance, . should not be jumped over).

Hi, I'm not an expert in Alloy at all so forgive me if I'm doing something obviously stupid.
Alloy 5 can't find instances for the bingo and win5InARow predicates, while Alloy 4.2 does (correctly) find them.

sig Number{}

sig RowId{}{ #RowId = 3 }

sig Ticket{
	numbers : RowId -> some Number
}{
	//There are exactly 3 different rows
	#(numbers.Number) = 3
	//There are exactly 5 different numbers per row
	all r : RowId | #(numbers[r]) = 5
	//All numbers in a ticket are different
	#(RowId.numbers) = 15
}

sig Coordinator{
	tickets : some Ticket,
	drawn : set Number
}

pred win5InARow[c: Coordinator, t: Ticket] {
	some r: RowId | t in c.tickets and r in t.(numbers.Number) and
	t.numbers[r] in c.drawn
}

pred bingo[c: Coordinator, t: Ticket] {
	t in c.tickets and
	all r: RowId | r in t.(numbers.Number) and t.numbers[r] in c.drawn
}

pred draw [g, g' : Coordinator, num : Number]{
	//precondition
	not num in g.drawn
	//postcondition
	g'.tickets = g.tickets
	g'.drawn = g.drawn + num
}

pred show{}

// run show for 20 but 1 Coordinator, 2 Ticket
// run draw for 20 but 2 Coordinator, 3 Ticket
// run win5InARow for 20 but 1 Coordinator, 3 Ticket
run bingo for 20 but 2 Coordinator, 3 Ticket

I'm running both versions on Arch Linux, java-8-openjdk, with default settings.

Let me know what additional information I can provide to help troubleshooting.

Hello!
I am working on a new application to work with alloy code, I'm using a combination of JavaFX & Javascript that allows me to use Monaco so to have intellisense, snippets and many other goodies.

Is there someone else who is working on something similar?

Attached a screenshot of the "alpha" :)

Some modules impose their formal parameter to be exact. E.g. util/ordering starts with:

module util/ordering[exactly elem]  

IMO when executing a command, the user should be warned if the corresponding signature(s) have not been explicitly specified as exact in the command. The rationale is to avoid situations where the user does not realize she has forgotten this exactness.
So, provided S is ordered, this should yield a warning:

run cmd1 for 5

and this should not:

run cmd1 for 5 but exactly 5 S

The following model seems to generate a solution that has instances for abstract sigs.

abstract sig B {}
abstract sig A {}
some sig A1 in A+B {}

run { some a : A1 | a in A or a in B } for 3 int

Which gives:

┌──┬──┬──┬──┬─┬─┬─┬─┬──┬──┐⁻¹
│-1│-2│-3│-4│0│1│2│3│A⁰│B⁰│  
└──┴──┴──┴──┴─┴─┴─┴─┴──┴──┘  

Not sure I understand this result. It seems to violate the some A1 and the abstractness?

About Couldn't open modules which is an alloy module file as markdown style, the issue has been closed.

I've tried SNAPSHOT.
But I got the same error.

Please reconfirm this patch.
I guess the path "Util.jarPrefix() + "models/" is wrong, isn't it?
I'd like to execute .md under my project directory.

Alloy4.2 fails to run the following check. I've checked a number of old Alloy versions and it seems this problem exists from the beginning.

module grandpa

abstract sig Person {}

sig Man extends Person { wife: lone Woman }

sig Woman extends Person { husband: lone Man }

check { no *(wife+husband)} for 1

From: N. Danas, T. Nelson, L. Harrison, S. Krishnamurthi, and D.J. Dougherty
User Studies of Principled Model Finder Output

Misleading Visualization Alloy’s model-visualization can impact understanding. We see several ways in which this output might have caused more maximal-group students to pick the erroneous edit; these suggest future studies. Figure 1 shows the first maximal model that students saw. Even though this model contains cycles of length 2 and 3, the immediacy and prominence of the 3 self-loops draws the eye. This may have led students in the maximal-model group to jump to the conclusion that self-loops (not cycles in general) were the problem to be fixed. Moreover, Alloy’s visualizer represents cycles of length 2 as a single, double-headed arrow. It is easy to not notice that the line represents a pair of (cycle-inducing) edges. In addition, the small arrowheads are easy to miss. Furthermore, self-loops and 2-cycles are explicit, requiring only one visual object to communicate. In contrast, cycles of size 3 and above are implicit; users must follow directed edges through multiple nodes to discover the cycle. This may lead to a tendency to pick out shorter cycles and miss larger ones.

It is now difficult to verify if two predicates are the same.

  pred a {...}
  pred b {...}

  pred equal { a = b } // fails

This then requires something like:

  pred equal { a => b else !b }

Which is kind of complexifying. I understand that it is caused by not exposing the primitive boolean to the language but I am not sure I understand why? Booleans are a common type. Although they are often abused (in Java booleans should often be an enum) they have their use. Especially here

Can someone clarify the role of the field nameExpr of class Command?
For this command

check TT{ some foo : Foo | some foo.next }

the nameExpr field is an ExprUnary with this .toString(): "(some foo | some foo.next)" and an ExprBadJoin subexpression.

I'm asking because this causes visitExpressions() on the containing module to fail, which causes hover and doNav operations in OurSyntaxWidget to fail.

The Alloy tool nicely color-codes reserved words. When I copy text from the Alloy tool and paste the text into Powerpoint, the color-coding is lost. Please provide a way to copy the text such that it can be pasted into Powerpoint (or Word) without losing the color-coding (formatting).

My code looks like below.

open util/ordering[Student]

enum Type { X, Y }

abstract sig Student{
        T : Type,
        TransHistory: set TransRecord
}
sig StudentX extends Student{
}{
        T = X
}
sig StudentY extends Student{
}{
        T = Y
}

sig TransRecord{
}

pred init(s: Student){
        no s.TransHistory
}

fact traces{
        first.init
        all s: Student - last | let s' = s.next |
                some x: TransRecord |
                        s'.TransHistory = s.TransHistory + x and s'.T = s.T
}

run {} for 5

I projected about Student and executed tracing, it was traced as 0 -> 1 -> 2 ...
However, when checked in the evaluation environment, it is as follows.

Student<:first => StudentX$2
Student<:first.next => StudentX$4
Student<:first.next.next => StudentX$0
Student<:first.next.next.next => StudentX$3
Student<:first.next.next.next.next => StudentX$1

In other words, it became random internally and it seemed that the meaning did not go through as trace.

I understand the reason.
It is because it orders Student and it is not attached to StudentX.
But, then, I think that I want the execution trace to be displayed in order of the student being ordered, and I think that is more reasonable.

The new Markdown format support is great, but the GUI only allows you to open files with a .als extension, not a .md extension.

Create a Mac executable in the dist project

The cursor is one character to the right from the position that's actually changed.

Example:

My text  |
         ^here is the cursor

Now I type the next word "is" and the result is:

My textis |

The blank after "text" disappears and is now after "is"

Environment: MacOSX 10.13.4

This issue is found in Alloy4.2 with SAT4J solver.

For example, I have the following Alloy model that models a directed tree:

module dtree
sig Node {
  edges: set Node
}
pred isDirectedTree {
  -- acyclic:
  no iden & ^edges
  -- injective: with mutation of the correct formula "edges.~edges in iden"
  edges.~edges != iden 
  -- connected:
  (Node -> Node) in ^(edges + ~edges)
}

If I run the following test

pred test {
  no Node
  no edges
  isDirectedTree[]
}
run test for 4

together with the model in side a single file (dtree.als), I got no instance with 439 vars. 20 primary vars. 636 clauses.

However, if I save the test in a separate file (test.als) and open the dtree module as shown below:

open dtree
pred test {
  no Node
  no edges
  isDirectedTree[]
}
run test for 4

I got an instance found with 449 vars. 24 primary vars. 642 clauses. When I inspect the instances, I found that the univ set = {Univ$0, ...} and all other sets are empty. I have no idea where do those Univ$i come from and I think separating the test predicate to a different file should behave the same as it is in the same file with the model. Please clarify or correct the behavior.

Below is a summary of the issue that Tim identified.

// When a pred is invoked (not run directly),
// then there is no type-checking to see that
// the type of the arguments matches the type
// of the pred's parameters. See section B.6.4
// of Software Abstractions for more info.
 
// Here is an example to illustrate:
sig A {}
sig A2 extends A {}
 
pred test1[x: A2] { }
 
// Invoke the pred with a value that is
// not in A2 (e.g., A - A2). The Alloy Analyzer generates
// an instance. That is, the pred is satisfiable (SAT).
// The reason that no error is generated is
// because no type-checking is done to check
// that the type of the argument matches the
// type of the pred's parameter.
run {some x: A - A2 | test1[x]}
 
pred test2[x: A2] {
  x not in A2
}
 
// When a pred is invoked directly (use the run command),
// then the constraints in the pred's parameters are AND'ed
// to the constraints in the pred's body. In pred test2 the
// constraints specify: (x is in A2) AND (x is not in A2). Obviously,
// there are no instances which satisfies that constraint, That is,
// the pred is not satisfiable (UNSAT).
run test2

I occasionally lose my work because I forget to reload before making changes to a file when I switch back to Alloy from another editor.
When a file is about to be saved, Alloy can use the file modification date to check if it has been modified since last loaded and give a warning.

For Alloy4.2, suppose I have a model called nqueens.als as follows:

module nqueens

sig Queen {
  row : Int,
  col: Int
}

pred noThreat(q1,q2 : Queen) {
  minus[q1.row, q2.row] != minus[q1.col,q2.col]
}

run noThreat

which implicitly import the util/integer module, but if I create another model called test.als as follows:

open nqueens

pred test() {
  some disj Q1, Q2: Queen {
    Queen = Q1 + Q2
    row = Q1->0 + Q2->1
    col = Q1->0 + Q2->1
    noThreat[Q1, Q2]
  }
}

run test

and if I execute run test then I get

A syntax error has occured:
The name "minus" cannot be found

It seems Alloy does not support transitive importing or may be Alloy only import integer module when it detects any use of Int type. But I believe this is unexpected.

Moreover, if I add open util/integer to the nqueens.als, both models compile. However, if I use CompUtil.parseEverything_fromFile to parse nqueens.als, it actually contains two open declaration:

open util/integer [] as integer
open util/integer [] as open$2

Shouldn't there be only one open integer declaration? This bothers me because my tool depends on Alloy AST and currently I need to filter out open declarations that includes $. Could you please fix all the above issues? Thanks.

Discovered here.

one sig PositiveEven {
     elements: set Int 
}

pred defining_property {
    PositiveEven.elements = {i: Int | i >= 0 and (rem[i,2] = 0)}
}

pred generate_set_members {
    0 in PositiveEven.elements
    all i: PositiveEven.elements - 0 | i.minus[2] in PositiveEven.elements
    // Create a complete set of positive even elements
    all i: Int | i.minus[2] in PositiveEven.elements => i in PositiveEven.elements
}

assert equivalent_constraints {
    generate_set_members => defining_property
}

check equivalent_constraints

On Windows 10, 4.2 finds a counterexample but 4.2_2015-02-22 does not. Both versions produce the same Kodkod under "Sat Solver > Output Kodkod to File", but different CNFs under "Sat Solver > Output CNF to File".

Since this repo doesn't have the complete repo history of alloy, I used this commit as a copy of 4.2 and this as 4.2_2015. My guess is that the issue is somewhere in fol2sat, possibly no earlier than Translator.java.* But I haven't built this from source to check because I, uh, don't actually know Java :( For the same reason, I haven't checked whether or not this is still a bug in master.

*My reasoning is that "Output CNF" constructs the Kodkod just like "Output Kodkod" does, but "Output CNF" also makes a call to Translator.

Will require getting a list of all people that contributed

I installed Alloy-5.0.0.1 on windows 10 system.
And I try the new feature - markdown syntax.

My tring code are:

---
title: Foo
layout: default
---

```alloy
sig Foo{
}
```

and

---
title: Bar
layout: default
---

```alloy
open Foo
```

I succeed to execute Foo.md on my alloy analyzer.
But I got error at executing Bar.md and alloy analyzer highlighted my code 'open Foo' line.

Starting the solver...

A syntax error has occured:
This module cannot be found.
It is not a built-in library module, and it cannot be found
at
"C:\Users\cut-sea\project\alloy\study-for-curriculum-by-alloy\Foo.als".

Could i import my Foo.md as markdown style ?

Following works in v.4.2 but not in in the "temporary release" from early April.2018:

assert intCheck {
no i: Int | i > 1 implies i > 0
}
check intCheck

(Along with the already present Search command)

Currently native libraries are included directly. We should build them from scratch.

Question: Is native code needed since sat4j seems to work very well?

When integers are used, not necessarily with explicit constants but also when the # operator is used, when arithmetic operations are used, etc., there is a risk of distortion of results when executing commands, because the bitwidth could be wrong for the problem.

To minimize errors here (in particular for newcomers), I think something should be done:

• either by emitting a reminder warning recalling that the bitwidth should be well thought out
• or by requiring an explicit bitwidth to be set in the scope of commands (and then failing otherwise)

Hi all,
Being an adept on alloy, i have an issue using alloy jar to translate an alloy description to a cnf file.
the code bellow can be used with sat4J and gives the output. but when using CNF i get no output.
Any tips on how to optain the output within a file "resultfile.cnf for example"
thank you.

import edu.mit.csail.sdg.alloy4.A4Reporter;
import edu.mit.csail.sdg.alloy4.Err;
import edu.mit.csail.sdg.alloy4.ErrorWarning;
import edu.mit.csail.sdg.alloy4compiler.ast.Command;
import edu.mit.csail.sdg.alloy4compiler.ast.Module;
import edu.mit.csail.sdg.alloy4compiler.parser.CompUtil;
import edu.mit.csail.sdg.alloy4compiler.translator.A4Options;
import edu.mit.csail.sdg.alloy4compiler.translator.A4Solution;
import edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod;

public final class Cli {

public static void main(String[] args)  {

    A4Reporter rep = new A4Reporter() {};
    String filename = args[0];
        Module world = CompUtil.parseEverything_fromFile(rep, null, filename);
        A4Options options = new A4Options();
        options.solver = A4Options.SatSolver.CNF;
        for (Command command : world.getAllCommands()) {
        A4Solution ans = TranslateAlloyToKodkod.execute_command(rep, world.getAllReachableSigs(), command, options);

        }

}

}

I just downloaded Alloy. After installing the legacy JDK as required when run on High Sierra, I can open the tool, but then any key press will produce a window saying "Sorry, a fatal internal error has occurred". I have sent the bug report, but thought that I would post the issue here too, just in case others search for it.

When typing some names, Alloy could propose some completion after 3 characters.

I have been encountering this problem for more than one year now: whenever I open the visualizer, no matter what spec it is (even sig A {} run {}), top shows that CPU resources are all taken up by the Xorg and java processes. If I leave the visualizer open for a minute, my CPU fan will become really loud. The visualizer is also very sluggish. Note that this only happens whenever the visualizer is open. It does not happen during solving. And when the problem happens, if I close the visualizer, the problem goes away.

This affects both Alloy 5.0 and 4.2. I am using Thinkpad X1 Yoga, Ubuntu 17.10, but it affects 17.04 as well. My Java version is:

java version "1.8.0_161"
Java(TM) SE Runtime Environment (build 1.8.0_161-b12)
Java HotSpot(TM) 64-Bit Server VM (build 25.161-b12, mixed mode)

For what it's worth: running the JAR with the option -Dsun.java2d.xrender=false makes the visualizer less sluggish, though it still consumes a lot of CPU resources. It also fixes a possibly related bug: whenever I rotate my screen and open the JAR normally, I get the following error:

Exception: class java.lang.ClassCastException
Message: java.lang.ClassCastException: sun.awt.image.BufImgSurfaceData cannot be cast to sun.java2d.xr.XRSurfaceData
Stacktrace:
class java.lang.ClassCastException: sun.awt.image.BufImgSurfaceData cannot be cast to sun.java2d.xr.XRSurfaceData
sun.java2d.xr.XRPMBlitLoops.cacheToTmpSurface(XRPMBlitLoops.java:148)
sun.java2d.xr.XrSwToPMBlit.Blit(XRPMBlitLoops.java:356)
sun.java2d.SurfaceDataProxy.updateSurfaceData(SurfaceDataProxy.java:498)
sun.java2d.SurfaceDataProxy.replaceData(SurfaceDataProxy.java:455)
sun.java2d.SurfaceData.getSourceSurfaceData(SurfaceData.java:233)
sun.java2d.pipe.DrawImage.renderImageCopy(DrawImage.java:566)
sun.java2d.pipe.DrawImage.copyImage(DrawImage.java:67)
sun.java2d.pipe.DrawImage.copyImage(DrawImage.java:1014)
sun.java2d.pipe.ValidatePipe.copyImage(ValidatePipe.java:186)
sun.java2d.SunGraphics2D.drawImage(SunGraphics2D.java:3318)
sun.java2d.SunGraphics2D.drawImage(SunGraphics2D.java:3296)
com.sun.java.swing.plaf.gtk.GTKEngine.paintCachedImage(GTKEngine.java:555)
com.sun.java.swing.plaf.gtk.GTKPainter.paintScrollBarBackground(GTKPainter.java:1055)
javax.swing.plaf.synth.SynthPainter.paintScrollBarBackground(SynthPainter.java:1021)
javax.swing.plaf.synth.SynthScrollBarUI.update(SynthScrollBarUI.java:241)
javax.swing.JComponent.paintComponent(JComponent.java:780)
javax.swing.JComponent.paint(JComponent.java:1056)
javax.swing.JComponent.paintChildren(JComponent.java:889)
javax.swing.JComponent.paint(JComponent.java:1065)
javax.swing.JComponent.paintChildren(JComponent.java:889)
javax.swing.JSplitPane.paintChildren(JSplitPane.java:1047)
javax.swing.JComponent.paint(JComponent.java:1065)
javax.swing.JComponent.paintChildren(JComponent.java:889)
javax.swing.JComponent.paint(JComponent.java:1065)
javax.swing.JComponent.paintChildren(JComponent.java:889)
javax.swing.JComponent.paint(JComponent.java:1065)
javax.swing.JLayeredPane.paint(JLayeredPane.java:586)
javax.swing.JComponent.paintChildren(JComponent.java:889)
javax.swing.JComponent.paint(JComponent.java:1065)
javax.swing.JComponent.paintToOffscreen(JComponent.java:5210)
javax.swing.BufferStrategyPaintManager.paint(BufferStrategyPaintManager.java:290)
javax.swing.RepaintManager.paint(RepaintManager.java:1272)
javax.swing.JComponent._paintImmediately(JComponent.java:5158)
javax.swing.JComponent.paintImmediately(JComponent.java:4969)
javax.swing.RepaintManager$4.run(RepaintManager.java:854)
javax.swing.RepaintManager$4.run(RepaintManager.java:814)
java.security.AccessController.doPrivileged(Native Method)
java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:80)
javax.swing.RepaintManager.paintDirtyRegions(RepaintManager.java:814)
javax.swing.RepaintManager.paintDirtyRegions(RepaintManager.java:789)
javax.swing.RepaintManager.prePaintDirtyRegions(RepaintManager.java:738)
javax.swing.RepaintManager.access$1200(RepaintManager.java:64)
javax.swing.RepaintManager$ProcessingRunnable.run(RepaintManager.java:1732)
java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:311)
java.awt.EventQueue.dispatchEventImpl(EventQueue.java:756)
java.awt.EventQueue.access$500(EventQueue.java:97)
java.awt.EventQueue$3.run(EventQueue.java:709)
java.awt.EventQueue$3.run(EventQueue.java:703)
java.security.AccessController.doPrivileged(Native Method)
java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:80)
java.awt.EventQueue.dispatchEvent(EventQueue.java:726)
java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:201)
java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:116)
java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:105)
java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)
java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:93)
java.awt.EventDispatchThread.run(EventDispatchThread.java:82)

Running the JAR with -Dsun.java2d.xrender=false fixes the problem.

there is a check for usage of integers and a check for usage of strings. These checks visit the AST but do not take into account that it can hold recursion. They therefore loop infinitely.

I tested it with a VisitQueryOnce class that extends VisitQuery but will return null on any visited node. This seemed to solve the problem.

If you're ok I can commit those changes but since is this is at the hard of Alloy I think you need to own this bug

Executing java -jar alloy.jar throws

Exception: class java.lang.NoSuchMethodError
Message: java.lang.NoSuchMethodError: com.apple.eawt.Application.addPreferencesMenuItem()V
Stacktrace:
class java.lang.NoSuchMethodError: com.apple.eawt.Application.addPreferencesMenuItem()V
edu.mit.csail.sdg.alloy4whole.SimpleGUI.<init>(SimpleGUI.java:1686)
edu.mit.csail.sdg.alloy4whole.SimpleGUI.<init>(SimpleGUI.java:203)
edu.mit.csail.sdg.alloy4whole.SimpleGUI$7.run(SimpleGUI.java:1659)
java.desktop/java.awt.event.InvocationEvent.dispatch(InvocationEvent.java:313)
java.desktop/java.awt.EventQueue.dispatchEventImpl(EventQueue.java:764)
java.desktop/java.awt.EventQueue.access$500(EventQueue.java:97)
java.desktop/java.awt.EventQueue$3.run(EventQueue.java:717)
java.desktop/java.awt.EventQueue$3.run(EventQueue.java:711)
java.base/java.security.AccessController.doPrivileged(Native Method)
java.base/java.security.ProtectionDomain$JavaSecurityAccessImpl.doIntersectionPrivilege(ProtectionDomain.java:89)
java.desktop/java.awt.EventQueue.dispatchEvent(EventQueue.java:734)
java.desktop/java.awt.EventDispatchThread.pumpOneEventForFilters(EventDispatchThread.java:199)
java.desktop/java.awt.EventDispatchThread.pumpEventsForFilter(EventDispatchThread.java:124)
java.desktop/java.awt.EventDispatchThread.pumpEventsForHierarchy(EventDispatchThread.java:113)
java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:109)
java.desktop/java.awt.EventDispatchThread.pumpEvents(EventDispatchThread.java:101)
java.desktop/java.awt.EventDispatchThread.run(EventDispatchThread.java:90)

The A4Preferences has a list of memory amounts to allocate for the native SAT solvers. This list needs to be updated for more reasonable values on todays machines, maybe even calcualated based on the available memory?

Or removed and always calculate it? Why skimp on memory when it is there anyway?

Create an executable for Windows

At edu.mit.csail.sdg.alloy4.OurConsole.style(OurConsole.java:133) the AlloyGraphics class is used:

fontName = AlloyGraphics.matchBestFontName(fontName);

but that class is not included in the final jar.

Hi, the Alloy GUI gets really slow on my computer.

How can I help solve it? I have little knowledge of debugging/profiling Java UI code.

I run ubuntu 16 with the gnome desktop manager.

Currently options are defined per user. An option like overflow detection can significantly change the run's and asserts in a model. I think we need to define any option that changes the outcome to a pragma so that models do not depend on user settings.

sig MySig {
  eq: set MySig
}

fact {
  iden in eq
}

This bombs out while generating the CNF. It's probably possible to catch with the type checker, as iden has a larger type than eq.

This is of course easy to fix with

fact { 
    (MySig->MySig & iden) in eq
}

but it took me a few minutes to understand the error.