How to model a consitent database in alloy?
up vote
0
down vote
favorite
Alloy newbie here. I'm trying to model a medical database containing user and some medical information.
sig User{
name: one String,
surname: one String,
socialNumber: one String,
address: one String,
age: one Int,
registration: one UserCredential,
healthStatus: one HealthInformation
}{
age>0
}
sig UserCredential{
user: one String,
pass: one String,
mail: one String
}
sig HealthInformation{}
sig Data4Help{
users: some User,
}
pred show(d:Data4Help){
#d.users>1
}
run show for 10
The analyzer tell me the model is inconsistent:
Executing "Run show for 10"
Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20
5448 vars. 510 primary vars. 12578 clauses. 16ms.
No instance found. Predicate may be inconsistent. 0ms.
Can you guys tell me why? All I want is having the database "Data4Help" linked to some users, probably the definition of the relation is incorrect but I don't know why.
Thank you
modeling alloy
asked Nov 10 at 16:56
Baratz96
11
add a comment |
up vote
0
down vote
favorite
Alloy newbie here. I'm trying to model a medical database containing user and some medical information.
sig User{
name: one String,
surname: one String,
socialNumber: one String,
address: one String,
age: one Int,
registration: one UserCredential,
healthStatus: one HealthInformation
}{
age>0
}
sig UserCredential{
user: one String,
pass: one String,
mail: one String
}
sig HealthInformation{}
sig Data4Help{
users: some User,
}
pred show(d:Data4Help){
#d.users>1
}
run show for 10
The analyzer tell me the model is inconsistent:
Executing "Run show for 10"
Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20
5448 vars. 510 primary vars. 12578 clauses. 16ms.
No instance found. Predicate may be inconsistent. 0ms.
Can you guys tell me why? All I want is having the database "Data4Help" linked to some users, probably the definition of the relation is incorrect but I don't know why.
Thank you
modeling alloy
asked Nov 10 at 16:56
Baratz96
11
add a comment |
up vote
0
down vote
favorite
up vote
0
down vote
favorite
Alloy newbie here. I'm trying to model a medical database containing user and some medical information.
sig User{
name: one String,
surname: one String,
socialNumber: one String,
address: one String,
age: one Int,
registration: one UserCredential,
healthStatus: one HealthInformation
}{
age>0
}
sig UserCredential{
user: one String,
pass: one String,
mail: one String
}
sig HealthInformation{}
sig Data4Help{
users: some User,
}
pred show(d:Data4Help){
#d.users>1
}
run show for 10
The analyzer tell me the model is inconsistent:
Executing "Run show for 10"
Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20
5448 vars. 510 primary vars. 12578 clauses. 16ms.
No instance found. Predicate may be inconsistent. 0ms.
Can you guys tell me why? All I want is having the database "Data4Help" linked to some users, probably the definition of the relation is incorrect but I don't know why.
Thank you
modeling alloy
asked Nov 10 at 16:56
Baratz96
11
Alloy newbie here. I'm trying to model a medical database containing user and some medical information.
sig User{
name: one String,
surname: one String,
socialNumber: one String,
address: one String,
age: one Int,
registration: one UserCredential,
healthStatus: one HealthInformation
}{
age>0
}
sig UserCredential{
user: one String,
pass: one String,
mail: one String
}
sig HealthInformation{}
sig Data4Help{
users: some User,
}
pred show(d:Data4Help){
#d.users>1
}
run show for 10
The analyzer tell me the model is inconsistent:
Executing "Run show for 10"
Solver=sat4j Bitwidth=4 MaxSeq=7 SkolemDepth=1 Symmetry=20
5448 vars. 510 primary vars. 12578 clauses. 16ms.
No instance found. Predicate may be inconsistent. 0ms.
Can you guys tell me why? All I want is having the database "Data4Help" linked to some users, probably the definition of the relation is incorrect but I don't know why.
Thank you
modeling alloy
modeling alloy
asked Nov 10 at 16:56
Baratz96
11
asked Nov 10 at 16:56
Baratz96
11
edited Nov 10 at 17:10
asked Nov 10 at 16:56
Baratz96
11
asked Nov 10 at 16:56
Baratz96
11
asked Nov 10 at 16:56
Baratz96
11
11
add a comment |
add a comment |
active
oldest
votes
active
oldest
votes
active
oldest
votes
active
oldest
votes
active
oldest
votes
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53241243%2fhow-to-model-a-consitent-database-in-alloy%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
