younes-io

----------------------------- MODULE TokenRing -----------------------------

EXTENDS Naturals, Sequences

CONSTANT N, Data, NULL, MaxLength

ASSUME N > 0

Nodes == 1..N

younes-io

### A Pluto.jl notebook ###
# v0.19.42

using Markdown
using InteractiveUtils

# ╔═╡ 4e348f70-7aa2-4d7f-b499-21fd7faaf8be
md"# I - Backpropagation done manually"

# ╔═╡ b45997c5-0c15-4c84-b6b3-3cc4518c968d

younes-io

Transaction_ID,Date,Customer_Name,Product,Total_Items,Total_Cost,Payment_Method,City,Store_Type,Discount_Applied,Customer_Category,Season,Promotion
1000000000,2020-12-21 19:42:52,Cheyenne Newman,['Hair Gel'],6,12.77,Debit Card,New York,Convenience Store,True,Student,Winter,None
1000000001,2020-07-06 07:45:16,Emily Fitzgerald,"['Tuna', 'Bread', 'Tissues', 'Trash Bags']",5,13.88,Debit Card,Houston,Supermarket,False,Professional,Fall,BOGO (Buy One Get One)
1000000002,2021-10-02 06:28:44,Michael Webb,"['Jam', 'Soap', 'Ketchup']",7,47.02,Debit Card,Miami,Convenience Store,False,Young Adult,Winter,None
1000000003,2022-01-10 05:39:02,Kimberly Lin,['BBQ Sauce'],9,83.86,Mobile Payment,Seattle,Warehouse Club,True,Senior Citizen,Summer,Discount on Selected Items
1000000004,2021-10-13 07:28:47,Cathy Hernandez,"['Hand Sanitizer', 'Bread', 'Extension Cords', 'Ice Cream', 'Hand Sanitizer']",4,30.55,Debit Card,Houston,Warehouse Club,False,Senior Citizen,Spring,None
1000000005,2021-04-26 20:45:13,Elizabeth Cook,"['Shower Gel'

younes-io

SSH keypair setup for GitHub (or GitHub/GitLab/BitBucket, etc, etc)

Create a repo.

Make sure there is at least one file in it (even just the README.md)

Generate a SSH key pair (private/public):

ssh-keygen -t rsa -C "your_email@example.com"

younes-io

--------------------------- MODULE BookingManager ---------------------------
\* 
\*  This is my TLA+ specification of a restaurant booking manager exercice
\* 
\* FEATURES:
\* - A user can add tables
\* - A table can get unlimited people (1..n)
\* - A user can set the time range of the open hours
\* - A user can add, edit or cancel reservations
\* 

younes-io

--------------------------- MODULE BookingManager ---------------------------
\* 
\*  This is my TLA+ specification of a restaurant booking manager exercice
\* 
\* FEATURES:
\* - A user can add tables
\* - A table can get unlimited people (1..n)
\* - A user can set the time range of the open hours
\* - A user can add, edit or cancel reservations
\* 

younes-io

-------------------------- MODULE SingleLaneBridge --------------------------

\* 
\*  This is my solution to the Single Lane Bridge problem in TLA+
\*  Also available in: https://github.com/tlaplus/Examples/blob/master/specifications/SingleLaneBridge/SingleLaneBridge.tla
\* 

\* A bridge over a river is only wide enough to permit a single lane of traffic.
\* Consequently, cars can only move concurrently if they are moving in the same 
\* direction. A safety violation occurs if two cars moving in different directions

younes-io

-------------------------- MODULE Readers_Writers --------------------------
\*https://en.wikipedia.org/wiki/Readers%E2%80%93writers_problem
EXTENDS Sequences, Naturals, FiniteSets
CONSTANTS Readers, Writers

VARIABLES Resource, semR, Waiting, semW
vars == <<Resource, semR, Waiting, semW>>

Range(S) == { S[i] : i \in DOMAIN S}