Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

add lobsters example #72

Merged
merged 1 commit into from
Oct 18, 2019
Merged

add lobsters example #72

merged 1 commit into from
Oct 18, 2019

Conversation

izgzhen
Copy link
Collaborator

@izgzhen izgzhen commented Oct 23, 2018

No description provided.

@izgzhen
Copy link
Collaborator Author

izgzhen commented Oct 23, 2018

the interesting thing is that:

_var2349 : Bag<Story> = stories

Lobsters:
  type HiddenToUser = { story_id : Int, user_id : Int }
  type StoryTag = { story_id : Int, tag_id : Int }
  type Vote = Vote
  type Story = Story
  state _var2349 : Bag<Story>

  query selectStoryVotes(p1 : Int, p2 : Int, p3 : Int, p4 : Int):
    Map {s -> (s, Map {v -> v} (Filter {v -> ((((v).val).user_id == p4) and (((v).val).comment_id == 0))} (((s).val).votes)))} (Filter {s -> ((((((((s).val).created_at > p3) and (not (exists Map {t -> t} (Filter {t -> ((t).tag_id == p2)} (((s).val).tags))))) and (not (exists Map {u -> u} (Filter {u -> ((u).user_id == p1)} (((s).val).hidden_to_users))))) and (((s).val).vote_count > 0)) and (((s).val).is_expired == false)) and (((s).val).merged_story_id == 0))} (_var2349))

  op insertVote(v : Vote):
    pass;

  op insertStory(s : Story):
    for _var3524 in []:
      _var2349.remove(_var3524);
    for _var3524 in [s]:
      _var2349.add(_var3524);

votes is optimized away by cozy -- I suspect that might be a bug.

@Calvin-L
Copy link
Collaborator

I don't think this is a bug in Cozy. Instead, I think this specification is not the one you intended. You have a votes member that is never read. The query selectStoryVotes reads s.val.votes, which is a different collection that never changes.

@Calvin-L
Copy link
Collaborator

I have added a note to #23 that Cozy should warn you about unused abstract state variables.

cozy/codegen/cxx.py Outdated Show resolved Hide resolved
@izgzhen
Copy link
Collaborator Author

izgzhen commented Oct 25, 2018

I've made this PR example-only

@Calvin-L
Copy link
Collaborator

The specification still has the unused votes member. Is that really what you intended?

@izgzhen
Copy link
Collaborator Author

izgzhen commented Oct 25, 2018

I don't think this is a bug in Cozy. Instead, I think this specification is not the one you intended. You have a votes member that is never read. The query selectStoryVotes reads s.val.votes, which is a different collection that never changes.
The specification still has the unused votes member. Is that really what you intended?

In reflection, there is a problem that I don't understand -- I uses assume all [ v in votes | v <- s.val.votes ]; in insertStory, which means at least after inserting, s should depend on votes. Accordingly, state stories should depend on votes, thus it seems buggy to me that votes is considered not used by Cozy.

@izgzhen
Copy link
Collaborator Author

izgzhen commented Oct 25, 2018

or put it another way, I don't know how to enforce the fact that votes in stories are aliases of votes in the spec states, by writing the spec in a particular way

@Calvin-L
Copy link
Collaborator

Collections in Cozy are value types, not references like they are in Java. To make them references you would need to wrap them in a handletype BagRef = Bag<Vote> and then use BagRef in many places.

@izgzhen
Copy link
Collaborator Author

izgzhen commented Oct 25, 2018

Collections in Cozy are value types, not references like they are in Java. To make them references you would need to wrap them in a handletype BagRef = Bag and then use BagRef in many places.

But Vote is already a reference type, isn't it? I don't need reference to this collection, instead, this collection holds references through which I can modify other values. Do I understand correctly?

@Calvin-L
Copy link
Collaborator

I see. The individual Vote objects may alias, not the collections that contain them.

The == operator on handle types checks reference equality, like it does in Java. You should be able to express your requirement along the lines of "for all stories, every vote in its votes bag is also in the central votes collection" or something.

@izgzhen
Copy link
Collaborator Author

izgzhen commented Oct 26, 2018

The == operator on handle types checks reference equality, like it does in Java. You should be able to express your requirement along the lines of "for all stories, every vote in its votes bag is also in the central votes collection" or something.

What do you mean? Do you mean that I should add an invariant?

@Calvin-L
Copy link
Collaborator

Yes, I meant that you should add an invariant. However, I see now that you already have the invariant all [ v in votes | s <- stories, v <- s.val.votes ]. So, disregard what I was saying.

Is it clear why insertVote does not affect s.val.votes for any story s? If not, we might need to provide clearer documentation about how Cozy understands the effect of statements like votes.add(v).

The statement votes.add(v) does not affect v, nor does it affect any object that references v. It only affects the votes collection, inserting the pointer value v. The invariant you wrote down says "every story's votes are a subset of votes." That invariant is trivially preserved by votes.add(v), which expands the votes collection but leaves every story's votes unchanged.

@Calvin-L
Copy link
Collaborator

I see that you added the invariant I suggested (although GitHub declined to notify me). I am merging this now; thanks for adding this example!

@Calvin-L Calvin-L merged commit ddcda0c into CozySynthesizer:master Oct 18, 2019
@izgzhen izgzhen deleted the lobsters branch October 21, 2019 19:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants