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 |
1 Answer
1
active
oldest
votes
up vote
1
down vote
The problem is that Alloy has some troubles with Strings. By default, the String signature defines an empty set of atoms. If you want to use Strings in your model, you will have to populate that set with "your own Strings".
See How to use String in Alloy?
In your model, you could add this simple fact
fact initPoolOfString
String in "insert"+ "your"+"dummy" + "strings" + "here"
answered Nov 19 at 14:02
Loïc Gammaitoni
3,310932
add a comment |
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
1
down vote
The problem is that Alloy has some troubles with Strings. By default, the String signature defines an empty set of atoms. If you want to use Strings in your model, you will have to populate that set with "your own Strings".
See How to use String in Alloy?
In your model, you could add this simple fact
fact initPoolOfString
String in "insert"+ "your"+"dummy" + "strings" + "here"
answered Nov 19 at 14:02
Loïc Gammaitoni
3,310932
add a comment |
up vote
1
down vote
The problem is that Alloy has some troubles with Strings. By default, the String signature defines an empty set of atoms. If you want to use Strings in your model, you will have to populate that set with "your own Strings".
See How to use String in Alloy?
In your model, you could add this simple fact
fact initPoolOfString
String in "insert"+ "your"+"dummy" + "strings" + "here"
answered Nov 19 at 14:02
Loïc Gammaitoni
3,310932
add a comment |
up vote
1
down vote
up vote
1
down vote
The problem is that Alloy has some troubles with Strings. By default, the String signature defines an empty set of atoms. If you want to use Strings in your model, you will have to populate that set with "your own Strings".
See How to use String in Alloy?
In your model, you could add this simple fact
fact initPoolOfString
String in "insert"+ "your"+"dummy" + "strings" + "here"
answered Nov 19 at 14:02
Loïc Gammaitoni
3,310932
The problem is that Alloy has some troubles with Strings. By default, the String signature defines an empty set of atoms. If you want to use Strings in your model, you will have to populate that set with "your own Strings".
See How to use String in Alloy?
In your model, you could add this simple fact
fact initPoolOfString
String in "insert"+ "your"+"dummy" + "strings" + "here"
answered Nov 19 at 14:02
Loïc Gammaitoni
3,310932
answered Nov 19 at 14:02
Loïc Gammaitoni
3,310932
answered Nov 19 at 14:02
Loïc Gammaitoni
3,310932
answered Nov 19 at 14:02
Loïc Gammaitoni
3,310932
3,310932
add a comment |
add a comment |
Thanks for contributing an answer to Stack Overflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Some of your past answers have not been well-received, and you're in danger of being blocked from answering.
Please pay close attention to the following guidance:
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
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
