CODEWITHSUNDEEP
alloy
John Wickerson
John Wickerson

Reputation: 1232

Alloy and Alloy* both fail on higher-order quantification

The following Alloy model:

sig A {}
run {all a : A | some r : A->A | a.r = a} for 3
run {some a : A | all r : A->A | a.r = a} for 3

fails for both Alloy and Alloy*. If I run both commands using ordinary Alloy (specifically, using the latest build from http://alloy.mit.edu/alloy/download.html, version 4.2_2015-02-22, build date 2015-02-22 18:21 EST), then the first command works fine but the second fails to skolemize:

output using ordinary Alloy

However, if I run both commands using Alloy* (specifically, using hola-0.2.jar from http://alloy.mit.edu/alloy/hola/), then the first command fails to skolemize and the second command works fine:

output using Alloy*

Perhaps there is some sort of bug here? I thought such problems were supposed not to happen in Alloy*; indeed, the Alloy* paper states that it "allows higher-order quantifiers to appear anywhere".

Upvotes: 1

Views: 198

Answers (1)

Aleksandar Milicevic
Aleksandar Milicevic

Reputation: 3867

Version 0.3 should work correctly.

Upvotes: 1

Related Questions