elliotswart/pragmaticformalmodeling

An instructional website with progressively worked examples of TLA+ specifications and model checking.

Pragmatic Formal Modeling

Getting Started

To test:

bundle install
bundle exec jekyll serve --incremental

To build:

bundle install
bundle exec jekyll build --incremental

Currently, the page is updated manually on Github pages, due to PlantUML dependency.

pragmaticformalmodeling's Issues

This is extremely good

That's all

Why use the operations var to express the a read have must have a write consistency?

Is it possible to use the temporal formula(using existing and universal symboler and action predicate and /\ and /) to express the consistency?
Look like the vars you specify is too many, specially about the observability vars?

Weak property cacherequirements!DatabaseAndCacheConsistent

pragmaticformalmodeling/caching/naive-model/cacherequirements.tla

Line 32 in ea86b1b

\/ cache[k] \in CacheMiss

Checking the property []<>DatabaseAndCacheConsistent with the definition where cache misses are permissible (above), is satisfied by, e.g., the trivial system of an always empty cache. For example, []<>DatabaseAndCacheConsistent holds with the CacheStartReadThroughFill disjunct removed from cacheinvalidationv3!CacheFairness. However, removing \/ cache[k] \in CacheMiss would obviously make the property too strong, since it would require all keys to be added to the cache.

The following two properties pass for cacheinvalidationv3, and appear to trigger the same counterexamples (please verify) for facebookcacheinvalidation, cacheinvalidationv1, and cacheinvalidationv2:

RepeatedlyCacheUsed ==
    []<>\E k \in DOMAIN cache: cache[k] \in CacheHit

RepeatedlyInSync ==
    []<>\A k \in DOMAIN cache: cache[k] \in CacheHit => cache[k].version = database[k]

PS: Nice real-world tutorial on TLA+!