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

Different results between alloy 5.0.0.201804081720 and stable 4.2 #71

Closed fcremo closed 5 years ago

fcremo commented 6 years ago

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.

vasil-sd commented 5 years ago

Everything is OK, you should just add '..., 5 Int' in 'run bingo for 20 but 2 Coordinator, 3 Ticket, 5 Int' It is the same problem, as described in https://stackoverflow.com/questions/51411209/why-cant-a-count-of-the-values-in-an-empty-field-be-compared-against-an-integer. Insufficient bits for Integers in the model. I suppose, that 4.2 version of Alloy has different default bitwidth for integers.