Skip to content

Commit

Permalink
Merge pull request #72 from izgzhen/lobsters
Browse files Browse the repository at this point in the history
add lobsters example
  • Loading branch information
Calvin-L authored Oct 18, 2019
2 parents b63e393 + 6120102 commit ddcda0c
Showing 1 changed file with 46 additions and 0 deletions.
46 changes: 46 additions & 0 deletions examples/lobsters.ds
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
// https://github.com/lobsters/lobsters
Lobsters:
type HiddenToUser = {
story_id : Int,
user_id : Int
}
type StoryTag = {
story_id : Int,
tag_id : Int
}
handletype Vote = {
id : Int,
user_id : Int,
comment_id : Int
}
handletype Story = {
merged_story_id : Int,
is_expired : Bool,
created_at : Int,
vote_count : Int,
hidden_to_users : Bag<HiddenToUser>,
tags : Bag<StoryTag>,
votes : Bag<Vote>
}
state stories : Bag<Story>
state votes : Bag<Vote>
invariant unique [ v.val.id | v <- votes ];
invariant all [ v in votes | s <- stories, v <- s.val.votes ];
query selectStoryVotes(p1: Int, p2 : Int, p3 : Int, p4 : Int)
[ (s, [ v | v <- s.val.votes,
v.val.comment_id == 0,
v.val.user_id == p4 ])
| s <- stories,
s.val.merged_story_id == 0,
s.val.is_expired == false,
s.val.vote_count > 0,
not (exists [ u | u <- s.val.hidden_to_users, u.user_id == p1 ]),
not (exists [ t | t <- s.val.tags, t.tag_id == p2 ]),
s.val.created_at > p3 ]
op insertVote(v : Vote)
assume not (exists [ v0 | v0 <- votes, v0.val.id == v.val.id ]);
votes.add(v);

op insertStory(s : Story)
assume all [ v in votes | v <- s.val.votes ];
stories.add(s);

0 comments on commit ddcda0c

Please sign in to comment.