parlarjb

  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"

........

parlarjb

---------------------------- MODULE Deployments ----------------------------
EXTENDS TLC, Integers

CONSTANT UPDATING, CORRUPT, ABORTED
CONSTANT SKIP_UPDATE

(* --algorithm deploy

variables servers = {"s1", "s2", "s3"},
          load_balancer = servers,

parlarjb

------------------------------ MODULE tlrouter ------------------------------
EXTENDS TLC, Sequences, Integers
(* --algorithm tlrouter
variables  
    input_stream = << [dest |-> "a", id |-> 1], [id |-> 1]>>,
    routing_table = <<>>, 

    output_streams = <<>>,
    dead_messages = {},
    msg;

parlarjb

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

parlarjb

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',

parlarjb

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

parlarjb

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

parlarjb

------------------------------- MODULE logger -------------------------------
EXTENDS Integers

CONSTANTS Clients

(*--algorithm logger

variables time = 0,
          log_start = [c \in Clients |-> 0];

parlarjb

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

parlarjb

one sig Person {
}

sig Resource {
  , access: set Person
  , parent: lone Resource
}

fact "No cycles" {