Alloy signatures not shown in Alloy Analyzer 4.2

Question

I have to use Alloy in a Requirements Analysis and Specification Document for a university project. I started with the easy stuff, only signatures and no facts. These are the signatures I use:

abstract sig Date{
    year: one Int,
    month: one Int,
    day: one Int
}

abstract sig Time{
    h: one Int,
    m: one Int,
    s: one Int
}

abstract sig Double{
    leftPart: one Int,
    rightPart: one Int
}

abstract sig Bool{
    value: one String
}

sig DateBirth extends Date{}
sig DateRide extends Date{}
sig DateExpiry extends Date{}


abstract sig User {
email: one String,
name: one String,
surname: one String,
gender: one Bool,
address: one String,
password: one String,
dateOfBirth: one DateBirth,
IDRide: set Ride
}

sig TaxiDriver extends User{
taxiLicense: one String,
personalLicense: one String,
IBAN: one String,
positionInQueue: lone Int,
IDTaxi: set Taxi
}


sig Client extends User{
}


sig Zone {
numberOfZone: one Int,
vertexNorthWest: one Double,
vertexNorthEast: one Double,
vertexSouthWest: one Double,
vertexSouthEast: one Double,
currentQueue: set TaxiDriver

}


sig Taxi {
IDTaxi: one String,
plate: one String,
availablePlaces: one Int,
}


sig Ride {
IDRide: one String,
origin: one String,
destination: one String,
dateOfRide: one DateRide,
timeOfDeparture: one Time,
timeOfArrival: one Time,
price: one Double,
numberOfPeople: one Int,
accepted: one Bool,
userEmail: set User
}


sig Credit_Card {
number: Double,
owner: String,
expiryDate: DateExpiry,
ownerEmail: one Client
}

Then, I added the predicate "show" to veify whether the it is consistent or not:

pred Show{}
run Show for 10

After running "Execute" on Alloy Analyzer 4.2 this is the message I get:

Executing "Run Show for 10"
   Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20
   21067 vars. 3840 primary vars. 37164 clauses. 376ms.
   Instance. found. Predicate is consistent. 375ms.

No problems, right? But then, when I click on "Show" there are no instances of the signature "User" (and its child signatures) shown on the display, while all the others are there. I tried to click on "Next" a gazillion times to try to see if maybe I could find a model in which they were shown, but there weren't any. Any idea/suggestion? Thanks!

Answer 1

It's probably because of the use of String. As far as I know, String is a reserved word in Alloy, but it is not really implemented at this point. Try to remove the String fields or replace them with something else.

On a more general note, Alloy is not so much about modelling real data (ints, bools and strings), but more about modelling structure, i.e. relationships between entities. For the analysis of structure, you usually don't need concrete data types.