| ericpony.github.io/z3py-tutorial/guide-examples.htm | |
| http://ericpony.github.io/z3py-tutorial/advanced-examples.htm | |
| https://theory.stanford.edu/~nikolaj/programmingz3.html | |
| A big tutorial: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.225.8231&rep=rep1&type=pdf | |
| http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.367.9961&rep=rep1&type=pdf | |
| Strategies/goals/tactics: http://www.cs.tau.ac.il/~msagiv/courses/asv/z3py/strategies-examples.htm | |
| Modelling a logic puzzle. Interesting because it uses uninterpreted functions https://stackoverflow.com/questions/53711168/modelling-a-logic-puzzle |
| ------------------------------- MODULE logger ------------------------------- | |
| EXTENDS Integers | |
| CONSTANTS Clients | |
| (*--algorithm logger | |
| variables time = 0, | |
| log_start = [c \in Clients |-> 0]; |
| sig FriendGroup { | |
| members: set Developer | |
| } | |
| sig Developer { | |
| // Each Developer is only working on zero or more Projects | |
| project: set Project, | |
| // The set of languages the developer enjoys using. | |
| // `some` means that there is at least one language in this set |
| EXTENDS Integers | |
| CONSTANT EMPTY | |
| (* | |
| The basic model is to map positions in a sequence to | |
| the squares on a tic-tac-toe board, as | |
| 1 | 2 | 3 | |
| --------- | |
| 4 | 5 | 6 |
| GIFS = ( | |
| 'https://gifs.parlar.ca/original/get_out.gif', | |
| 'https://gifs.parlar.ca/tongue/tongue-out.gif', | |
| 'https://gifs.parlar.ca/bring-it/luke-cage-bring-it.gif', | |
| 'https://gifs.parlar.ca/original/kick.gif', | |
| 'https://gifs.parlar.ca/original/nope_bobby.gif', | |
| 'https://gifs.parlar.ca/contempt/Dwight-Schrute-look-of-disapproval.gif', | |
| 'https://gifs.parlar.ca/original/no_josh.gif', | |
| 'https://gifs.parlar.ca/contempt/simon-cowel-glazed-look.gif', | |
| 'https://gifs.parlar.ca/no/nope-duck.gif', |
| module hallway | |
| open util/ordering[Time] | |
| sig Time {} | |
| abstract sig Position {} | |
| one sig Left, Right, Passed extends Position {} | |
| abstract sig Person { | |
| position: Position one -> Time |
| ------------------------------ MODULE tlrouter ------------------------------ | |
| EXTENDS TLC, Sequences, Integers | |
| (* --algorithm tlrouter | |
| variables | |
| input_stream = << [dest |-> "a", id |-> 1], [id |-> 1]>>, | |
| routing_table = <<>>, | |
| output_streams = <<>>, | |
| dead_messages = {}, | |
| msg; |
| ---------------------------- MODULE Deployments ---------------------------- | |
| EXTENDS TLC, Integers | |
| CONSTANT UPDATING, CORRUPT, ABORTED | |
| CONSTANT SKIP_UPDATE | |
| (* --algorithm deploy | |
| variables servers = {"s1", "s2", "s3"}, | |
| load_balancer = servers, |
| class Logger(object): | |
| def __enter__(self): | |
| return self | |
| def __exit__(self, exc_type, value, traceback): | |
| print "Logging some stuff" | |
| if exc_type is not None: | |
| print "Sending exception up to New Relic" | |
| ........ |
On Cloud Atlas, we switched to a heavily modified version of the “git flow” workflow, based on http://nvie.com/posts/a-successful-git-branching-model/ and https://www.atlassian.com/git/workflows#!workflow-gitflow
The basic premise is this: We run one main branch, develop, and whenever we want to begin preparing for a release, we create a Release_x.y.z branch off of develop. It is these Release_x.y.z branches that get deployed to staging and then production.