add lobsters example

[izgzhen]

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]

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]

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

[izgzhen]

I've made this PR example-only

[Calvin-L]

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

[izgzhen]

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]

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]

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]

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]

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]

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]

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]

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!