Подписи сплавов, не показанные в анализаторе сплавов 4.2

Question

Я должен использовать сплав в документе анализа требований и спецификации для университетского проекта. Я начал с простых вещей, только подписи и никаких фактов. Эти подписи, которые я использую:

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 
} 

Затем я добавил предикат «шоу», чтобы veify ли оно соответствует или нет:

pred Show{} 
run Show for 10 

После запуска «Выполнить» на Alloy Analyzer 4.2 это это сообщение, которое я получаю:

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. 

Нет проблем, не так ли? Но тогда, когда я нажимаю «Показать», на дисплее не отображаются экземпляры подписи «Пользователь» (и ее дочерние подписи), а все остальные. Я попытался щелкнуть «Далее», чтобы посмотреть, может ли я найти модель, в которой они были показаны, но их не было. Любая идея/предложение? Благодаря!

Answer 1

Возможно, это связано с использованием String. Насколько мне известно, String - это зарезервированное слово в Alloy, но на данный момент оно не реализовано. Попробуйте удалить поля String или заменить их на что-то еще.

В более общем плане, сплав - это не столько о моделировании реальных данных (ints, bools и strings), но и о моделировании структуры, т.е. отношений между объектами. Для анализа структуры вам обычно не нужны конкретные типы данных.

Answer 2

Целью построения модели сплава является захват сущности конструкции или системы и изучение тонких свойств. Вы не хотите включать все детали, которые вы найдете в схеме базы данных. В вашей модели также много деталей реализации, таких как идентификаторы (которые не нужны, поскольку они неявны в идентификаторах объектов), а использование строк вместо концептуальных типов - например, пункт назначения должен иметь тип такой как «Местоположение».

Так что я рекомендую вам начать заново и сначала подумать о том, какие вопросы вы хотите получить от этой модели.

Answer 3

Спасибо всем, удаляя строки решил проблему.

Однако мое «искаженное» видение цели Сплака было связано с тем, что нас попросили использовать его, но нам не дали реального объяснения того, как его использовать, в большинстве случаев все детали были написаны. Наверное, мне придется попробовать и изучить его еще немного!