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










share|improve this question



























    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










    share|improve this question

























      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










      share|improve this question















      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






      share|improve this question















      share|improve this question













      share|improve this question




      share|improve this question








      edited Nov 10 at 17:10

























      asked Nov 10 at 16:56









      Baratz96

      11




      11



























          active

          oldest

          votes











          Your Answer






          StackExchange.ifUsing("editor", function ()
          StackExchange.using("externalEditor", function ()
          StackExchange.using("snippets", function ()
          StackExchange.snippets.init();
          );
          );
          , "code-snippets");

          StackExchange.ready(function()
          var channelOptions =
          tags: "".split(" "),
          id: "1"
          ;
          initTagRenderer("".split(" "), "".split(" "), channelOptions);

          StackExchange.using("externalEditor", function()
          // Have to fire editor after snippets, if snippets enabled
          if (StackExchange.settings.snippets.snippetsEnabled)
          StackExchange.using("snippets", function()
          createEditor();
          );

          else
          createEditor();

          );

          function createEditor()
          StackExchange.prepareEditor(
          heartbeatType: 'answer',
          convertImagesToLinks: true,
          noModals: true,
          showLowRepImageUploadWarning: true,
          reputationToPostImages: 10,
          bindNavPrevention: true,
          postfix: "",
          imageUploader:
          brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
          contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
          allowUrls: true
          ,
          onDemand: true,
          discardSelector: ".discard-answer"
          ,immediatelyShowMarkdownHelp:true
          );



          );













           

          draft saved


          draft discarded


















          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






























          active

          oldest

          votes













          active

          oldest

          votes









          active

          oldest

          votes






          active

          oldest

          votes















           

          draft saved


          draft discarded















































           


          draft saved


          draft discarded














          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





















































          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







          Popular posts from this blog

          Top Tejano songwriter Luis Silva dead of heart attack at 64

          ReactJS Fetched API data displays live - need Data displayed static

          政党