Add 10 fizzbee model examples for lovable apps.

examples/requirements/lovable/01-todo-app/TodoApp.fizz

@@ -0,0 +1,137 @@
+---
+deadlock_detection: false
+options:
+    max_concurrent_actions: 1
+---
+
+# Personal Todo App — Requirements Specification
+# Architecture: React (browser) + Supabase (database)
+# Single user — verifies CRUD, toggle, filters, clear-completed
+#
+# Modeled after: /Users/jp/src/my-simple-todo (Lovable-generated)
+# DB schema: id (UUID), text, done (bool), created_at (timestamp)
+# Ordering: ORDER BY created_at ASC — modeled as list insertion order
+
+MAX_ITEMS = 3
+
+# IDs: nominal symmetric — like UUIDs, only equality matters
+IDS = symmetry.nominal(name="id", limit=MAX_ITEMS)
+
+# Texts: interchangeable task descriptions — specific wording doesn't affect behavior
+# Using choices() rather than materialize=True: avoids spurious branching on first add
+TEXTS = symmetry.nominal(name="task", limit=2)
+
+Filter = enum("All", "Pending", "Completed")
+
+
+# ─── Server (Database) ───────────────────────────────────────────────
+# Ground truth. Supabase Postgres with RLS.
+# Stored as a list to preserve insertion order (ORDER BY created_at ASC).
+
+role Server:
+    action Init:
+        self.todos = []
+
+    atomic func AddTodo(id, text):
+        self.todos = self.todos + [record(id=id, text=text, done=False)]
+
+    atomic func ToggleTodo(id):
+        updated = []
+        for t in self.todos:
+            if t.id == id:
+                updated = updated + [record(id=id, text=t.text, done=not t.done)]
+            else:
+                updated = updated + [t]
+        self.todos = updated
+
+    atomic func DeleteTodo(id):
+        self.todos = [t for t in self.todos if t.id != id]
+
+    atomic func ClearCompleted():
+        self.todos = [t for t in self.todos if not t.done]
+
+
+# ─── User (Human + Browser) ──────────────────────────────────────────
+# React frontend. Holds a filtered view refreshed after each mutation.
+# Filter is client-side state; view is derived from DB + filter.
+
+role User:
+    action Init:
+        self.filter = Filter.All
+        self.view = []
+        self.completed_exist = False
+
+    atomic func RefreshView():
+        if self.filter == Filter.All:
+            self.view = db.todos
+        elif self.filter == Filter.Pending:
+            self.view = [t for t in db.todos if not t.done]
+        else:
+            self.view = [t for t in db.todos if t.done]
+        self.completed_exist = len([t for t in db.todos if t.done]) > 0
+
+    # ── CRUD ──
+
+    atomic action AddTodo:
+        id = IDS.fresh()
+        text = any TEXTS.choices()
+        db.AddTodo(id, text)
+        self.RefreshView()
+
+    atomic action ToggleTodo:
+        require len(self.view) > 0
+        index = any range(len(self.view))
+        item = self.view[index]
+        db.ToggleTodo(item.id)
+        self.RefreshView()
+
+    atomic action DeleteTodo:
+        require len(self.view) > 0
+        index = any range(len(self.view))
+        item = self.view[index]
+        db.DeleteTodo(item.id)
+        self.RefreshView()
+
+    # ── Filter & bulk ──
+
+    atomic fair action SwitchFilter:
+        require len(db.todos) > 0
+        new_filter = fair any [f for f in dir(Filter) if self.filter != f]
+        self.filter = new_filter
+        self.RefreshView()
+
+    atomic action ClearCompleted:
+        require self.completed_exist
+        db.ClearCompleted()
+        self.RefreshView()
+
+
+# ─── Initialization ──────────────────────────────────────────────────
+
+action Init:
+    db = Server()
+    user = User()
+
+
+# ─── Safety Assertions ───────────────────────────────────────────────
+
+# R1: The displayed list always matches the current filter applied to the DB.
+#     Catches filter-logic bugs across all possible action sequences.
+always assertion ViewMatchesFilter:
+    if user.filter == Filter.All:
+        expected = db.todos
+    elif user.filter == Filter.Pending:
+        expected = [t for t in db.todos if not t.done]
+    else:
+        expected = [t for t in db.todos if t.done]
+    return user.view == expected
+
+# R2: The "Clear Completed" button visibility stays in sync with the DB.
+always assertion CompletedFlagConsistent:
+    has_completed = len([t for t in db.todos if t.done]) > 0
+    return user.completed_exist == has_completed
+
+# R3: No duplicate todo IDs.
+always assertion UniqueTodoIds:
+    ids = [t.id for t in db.todos]
+    return len(ids) == len(set(ids))

examples/requirements/lovable/02-poll/Poll.fizz

@@ -0,0 +1,133 @@
+---
+deadlock_detection: false
+options:
+    max_concurrent_actions: 1
+---
+
+# Poll / Voting App — Requirements Specification
+# Architecture: React (browser) + Supabase (database)
+#
+# A creator makes a poll with a fixed set of options. Multiple voters
+# can vote, change their vote, or abstain. The creator can close the poll.
+# Once closed, no more votes are accepted.
+#
+# New concepts: multiple symmetric users, shared mutable resource, close semantics
+
+NUM_VOTERS = 2
+
+# Options are interchangeable — which specific option a voter picks doesn't matter
+OPTIONS = symmetry.nominal(name="opt", limit=3)
+
+Status = enum("Open", "Closed")
+
+
+# ─── Server (Database) ───────────────────────────────────────────────
+# polls table: status, options (fixed set)
+# votes table: voter_id -> option (one vote per voter, can update)
+
+role Server:
+    action Init:
+        self.status = Status.Open
+        self.votes = {}
+
+    atomic func CastVote(voter_id, option):
+        require self.status == Status.Open
+        self.votes[voter_id] = option
+
+    atomic func RemoveVote(voter_id):
+        require self.status == Status.Open
+        require voter_id in self.votes
+        self.votes.pop(voter_id)
+
+    atomic func ClosePoll():
+        self.status = Status.Closed
+
+
+# ─── Voter (Human + Browser) ─────────────────────────────────────────
+# Each voter sees the poll and can vote/change/retract.
+# Voters are symmetric — they are interchangeable.
+
+role Voter:
+    action Init:
+        self.my_vote = None
+        self.poll_open = True
+
+    atomic func RefreshView():
+        self.poll_open = (db.status == Status.Open)
+        if self.__id__ in db.votes:
+            self.my_vote = db.votes[self.__id__]
+        else:
+            self.my_vote = None
+
+    atomic action Vote:
+        require self.poll_open
+        require self.my_vote == None
+        option = any OPTIONS.choices()
+        db.CastVote(self.__id__, option)
+        self.RefreshView()
+
+    atomic action ChangeVote:
+        require self.poll_open
+        require self.my_vote != None
+        new_option = any [o for o in OPTIONS.choices() if o != self.my_vote]
+        db.CastVote(self.__id__, new_option)
+        self.RefreshView()
+
+    atomic action RetractVote:
+        require self.poll_open
+        require self.my_vote != None
+        db.RemoveVote(self.__id__)
+        self.RefreshView()
+
+    atomic fair action RefreshPollStatus:
+        require self.poll_open and db.status == Status.Closed
+        self.RefreshView()
+
+
+# ─── Creator (poll owner) ────────────────────────────────────────────
+# The creator can close the poll. Not a voter in this model.
+
+role Creator:
+    action Init:
+        self.closed = False
+
+    atomic action ClosePoll:
+        require not self.closed
+        db.ClosePoll()
+        self.closed = True
+
+
+# ─── Initialization ──────────────────────────────────────────────────
+
+action Init:
+    db = Server()
+    creator = Creator()
+    voters = bag()
+    for i in range(NUM_VOTERS):
+        voters.add(Voter())
+
+
+# ─── Safety Assertions ───────────────────────────────────────────────
+
+# R1: After refresh, each voter's local my_vote matches the database.
+always assertion VoterViewConsistent:
+    for v in voters:
+        if v.__id__ in db.votes:
+            if v.my_vote != None and v.my_vote != db.votes[v.__id__]:
+                return False
+        else:
+            if v.my_vote != None and not v.poll_open:
+                return False
+    return True
+
+# R2: Once the poll is closed, the votes never change.
+transition assertion ClosedPollIsImmutable(before, after):
+    if before.db.status == Status.Closed:
+        return before.db.votes == after.db.votes
+    return True
+
+# R3: Once the poll is closed, it stays closed.
+transition assertion ClosedStaysClosed(before, after):
+    if before.db.status == Status.Closed:
+        return after.db.status == Status.Closed
+    return True

examples/requirements/lovable/03-booking/Booking.fizz

@@ -0,0 +1,101 @@
+---
+deadlock_detection: false
+options:
+    max_concurrent_actions: 1
+---
+
+# Booking App (Calendly-style) — Requirements Specification
+# Architecture: React (browser) + Supabase (database)
+#
+# A host creates available time slots. Guests browse slots and book one.
+# Race condition: two guests see the same slot as available, both try to book.
+# The database must prevent double-booking (only one guest per slot).
+#
+# New concepts: stale views, race condition, double-booking prevention
+
+NUM_GUESTS = 2
+NUM_SLOTS = 2
+
+SLOTS = symmetry.nominal(name="slot", limit=NUM_SLOTS)
+
+
+# ─── Server (Database) ───────────────────────────────────────────────
+# slots table: slot_id -> guest_id or None (None = available)
+
+role Server:
+    action Init:
+        self.slots = {}
+
+    atomic func BookSlot(slot_id, guest_id):
+        # RLS / server-side constraint: only book if available
+        require self.slots[slot_id] == None
+        self.slots[slot_id] = guest_id
+
+    atomic func CancelBooking(slot_id, guest_id):
+        require self.slots[slot_id] == guest_id
+        self.slots[slot_id] = None
+
+
+# ─── Guest (Human + Browser) ─────────────────────────────────────────
+# Sees a snapshot of available slots. By the time they click "Book",
+# another guest may have already taken the slot.
+
+symmetric role Guest:
+    action Init:
+        self.view_available = []
+        self.my_booking = None
+
+    atomic func RefreshView():
+        self.view_available = [s for s in db.slots if db.slots[s] == None]
+        # Check if I still have a booking
+        self.my_booking = None
+        for s in db.slots:
+            if db.slots[s] == self.__id__:
+                self.my_booking = s
+
+    # Guest sees available slots and picks one to book
+    atomic action BookSlot:
+        require self.my_booking == None
+        require len(self.view_available) > 0
+        slot = any self.view_available
+        db.BookSlot(slot, self.__id__)
+        self.RefreshView()
+
+    # Guest cancels their existing booking
+    atomic action CancelBooking:
+        require self.my_booking != None
+        db.CancelBooking(self.my_booking, self.__id__)
+        self.RefreshView()
+
+    # Guest refreshes their browser to see latest availability
+    atomic fair action Refresh:
+        self.RefreshView()
+
+
+# ─── Initialization ──────────────────────────────────────────────────
+# Host creates slots, then guests join. Slot creation is setup, not ongoing behavior.
+
+action Init:
+    db = Server()
+    for i in range(NUM_SLOTS):
+        slot_id = SLOTS.fresh()
+        db.slots[slot_id] = None
+    guests = bag()
+    for i in range(NUM_GUESTS):
+        guests.add(Guest())
+
+
+# ─── Safety Assertions ───────────────────────────────────────────────
+
+# R1: Each slot has at most one guest assigned.
+always assertion NoDoubleBooking:
+    booked_guests = [db.slots[s] for s in db.slots if db.slots[s] != None]
+    return len(booked_guests) == len(set(booked_guests))
+
+# R2: A guest holds at most one booking at a time.
+always assertion OneBookingPerGuest:
+    for g in guests:
+        count = len([s for s in db.slots if db.slots[s] == g.__id__])
+        if count > 1:
+            return False
+    return True