class: center, middle, title-slide count: false # Being Formal Yet Lightweight ## Alejandro Serrano @ DDD Europe 2021 .less-line-height[ 🌐 serras.github.io/dddeu21 - 🗂️ Miro .grey[🐦 @trupill - 👨‍💻 47 Degrees (Academy)] ] --- # 🥅 Our goal Turn our models into _propert artifacts_ (files) -- This means our model can be... - put in version control - inspected by proper tools - checked for consistency -- We want to do it in a _productive_ way --- # Electrum and Alloy Alloy is a modelling language - currently in version 5.1 -- Electrum extends Alloy with temporal logic - simpler ways to specify changes of state - currently 2.1.3, built on top of Alloy 5.1 -- Electrum is going to become Alloy 6 --- # Preparation .less-line-height[ 1. Download a Java Virtual Machine ```scala java.com/download ``` 2. Download Electrum ```scala github.com/haslab/Electrum2/releases ``` 3. Run the Jar you've downloaded ```scala java -jar electrum-2.1.3.jar ``` ] --- # Our first exploration Open Electrum and write the following <br /> (available for copy in the workshop repo) ```scala sig Person { } sig Course { teacher : Person, students : set Person } ``` -- > You have to love the Java vibe of the UI! ♨️ --- # Our first exploration Click _Execute_ ⚡  -- And then click .blue[_instance_] - works better if you detach the window -- ## This is where exploration begins! --- class: center, middle, title-slide # ⌛ Alloy / Electrum time! ??? 'Next' loops over instances Just point to this in the window Teacher overlaps with students Maybe no students --- # Identity In many cases, we only care about sth. _existing_ --  This is enough to point to a possible problem --- # Important advice ### Keep irrelevant details out of your model --   - Each `Person` has a name (first + last) - And each `Course` has an identifier - Which is a UUID autogenerated by the DB > Not important in this model! --- class: center, middle, title-slide # ⏲️ Alloy / Electrum time! ??? Introduce `#students > 0` Then talk about some / set / lone Introduce the invariant about teacher not a student `no t: teacher | t in students` And then rewrite to `no teacher & students` ```scala sig Person { } sig Course { teacher : Person, students : some Person } { no teacher & students } ``` --- # Everything is a set .margin-top[ - Every field (`teacher`, `students`) defines a set - Every signature (`Person`, `Course`) also ] -- ## What can you do with sets? _Use different multiplicities_ - `one` is the default - `lone` is at most one - `some` is at least one - `set` is any amount --- # Everything is a set .margin-top[ - Every field (`teacher`, `students`) defines a set - Every signature (`Person`, `Course`) also ] ## What can you do with sets? _Combine several of them_ - Intersection: `a & b` - Union: `a + b` - Difference `a - b` --- # Everything is a set .margin-top[ - Every field (`teacher`, `students`) defines a set - Every signature (`Person`, `Course`) also ] ## What can you do with sets? _Use them to bound a quantifier_ - `all x : set | ...` - `some x : set | ...`, or `some set` (not empty) - `no x : set | ...`, or `no set` (empty) - `one x : set | ...` --- class: center, middle, title-slide # 🧑‍💻 Practice time! -- > This is DDD Europe, so football ≡ soccer --- # ⚽ Football match model Write an Alloy / Electrum model: - We have _people_ - Some of them (how many?) form a _team_ - A _match_ has two teams and a _referee_ Explore the model and find weird corner cases Discuss and write down some facts > Collaborate in groups of 2 or 3 people 🙂 --- # Benefits of formal modelling A _documented_ artifact ... - Design changes require a pull request - Signals that code may need update 🚦 -- ... in a language understood by a _tool_ ... - Explore and check properties -- ... at a very _high-level_ - Focus on the domain, not on the details - As opposed to prototypes in code --- # Lightweight modelling No **full** formalization of the model - Usually a huge time and effort cost - Diminishing returns - Most models change anyway 🤷 -- > 10% effort for 90% better understanding! -- > (yep, this sentence is slightly nonsensical) --- # Counter-examples _Are our properties **correct** and **enough**?_ -- We can ask Electrum to find counter-examples! -- If they are not enough, _refine_ the model --- class: center, middle, title-slide # 🕰️ Alloy / Electrum time! ??? Introduce the concept of assertion Explain `check` to find a counterexample Talk about `for` as a way to measure effort ```scala assert NoTeacherIsStudent { all c1 : Course | no c2 : Course | c1.teacher in c2.students } check NoTeacherIsStudent for 3 ``` --- # Assertions vs. facts Facts **must** hold in _any_ model - In addition to multiplicity constraints - May appear in a signature or detached ```scala fact TeacherIsNotStudent { all c: Course | no c.teacher & c.students } ``` -- Assertions are **expected** to hold - They should be implied by the facts --- class: center, middle, title-slide # 🧑‍💻 Practice time! --- # ⚽ Football match model Introduce a notion of _week_ - All matches in the same week should have disjoint teams playing - A person can referee at most one match per week (but maybe none) --- # Referees and players _Referees should not be players, and viceversa_ -- ```scala abstract sig Person { } // no elements sig Referee extends Person { } sig Player extends Person { } ``` -- This is equivalent to subset + disjointness ```scala sig Referee in Person { } // subset sig Player in Person { } // subset fact DisjointPeople { no Referee & Player } ``` --- # Matches for a given week What should we choose? ```scala // a week is tied to a match sig Week { } sig Match { week : Week } // each week knows about its matches sig Match { } sig Week { matches : set Match } ``` --- # Matches for a given week Let's suppose we choose the first one ```scala // a week is tied to a match sig Week { } sig Match { week : Week } ``` _"Each week has at least one match"_ 🤔 -- ```scala fact EachWeekHasOneMatch { all w : Week | some week.w // post-join } ``` --- class: center, middle, title-slide # 🌀 Modelling time ## In Electrum, but not in Alloy (yet) --- # Modelling time You can talk about _operations_ and _events_ - A student wants to enroll in a course -- We use _temporal logic_ to express properties - "A student is never enrolled in a course before completing its prerequisites" - "A completed exercise is eventually graded" --- # 🛒 Cart model ## Describing a snapshot .margin-top[ - Availability of a set of products - A set of carts which: - Include products in some amount - May be "open" or "checked out" ] --- # 🛒 Cart model ## Describing a snapshot .margin-top[ - Availability of a ~~set of~~ product~~s~~ - A set of carts which: - Include _the_ product~~s~~ in some amount - May be "open" or "checked out" ] ## Simplify!! Enough to check the basic properties --- class: center, middle, title-slide # ⏱️ Alloy / Electrum time! ??? Introduce how to open a module Explain that you cannot have "global" properties Introduce enum ```scala open util/integer one sig Product { available: Int } enum Status { Open, CheckedOut } sig Cart { status: Status, amount: Int } ``` --- # Describing change 1. Mark some fields with `var` -- 2. Create predicates for each operation or event ```scala Product.available' // next state = minus[Product.availabe, c.amount] ``` -- 😪 You also need to describe **un**changes ```scala c.status' = c.status ``` --- class: center, middle, title-slide # ⌚ ~~Alloy~~ / Electrum time! ??? Explain each predicate as preconditions, changed, unchanged Write the final trace --- # Why <tt>skip</tt>? Traces in Electrum must be _infinite_ - Finite ones are represented by repeating a "do nothing" operation -- ## Useful on their own .margin-top[ - On a queue, a message is completely lost - The user never checks out a cart ] TLA+ calls these _stuttering_ steps --- class: center, middle, title-slide # 🕒 Electrum time! ??? Show a few assertions and counter-examples --- class: center, middle, title-slide # 🧑‍💻 Practice time! --- # 🏆 Football cup finals > _Eventually_ there must be a winner Model the protocol for goals - States: regular, extra time, penalty shoot-outs - If a team has more goals, that one wins Can you find a possible deadlock? --- class: center, middle, title-slide # Summary ## and Looking Forward --- # There's more! ## Set operators .margin-top[ - Transitive closures with `^` - The general definition of join `.` ] --- # There's more! ## Relational fields ```scala abstract sig Grade { } one sig Fail extends Grade { } sig Pass extends Grade { } sig Course { grades : Person -> one Grade } ``` And the awesome projection view! --- # Summary Electrum helps you _document_ your model - exploration of instances - consistency checks and counter-examples Both _statics_ and _dynamics_ can be modelled - Usual data models - Protocols, operations, and events --- class: center, middle, title-slide # 🙋 Questions and comments --- class: center, middle, title-slide # 🤩 It's been a pleasure ## Enjoy the rest of DDD Europe 2021!