travis (#3)

* travis stuff

* Update Makefile

* Update README.md

* Update SpecOK.cfg

* Update .travis.yml

* Update SpecOK.cfg

* test

* fix

* fix

* fix

* one more attempt

* maybe

* fix

* updated

.travis.yml

@@ -0,0 +1,22 @@
+language: c
+
+notifications:
+  email: false
+
+branches:
+  only:
+    - master
+
+before_install:
+  - |
+      if ! git diff --name-only $TRAVIS_COMMIT_RANGE | grep -qvE '(.md)|(.html)|^(LICENSE)|^(docs)'
+      then
+        echo "Only docs were updated, not running the CI."
+        exit 0
+      fi
+
+services:
+  - docker
+
+script:
+  - make

MVDS/MVDS.tla

@@ -3,7 +3,7 @@
 (*        TLA+ specification of Minimum Viable Data Synchronization        *)
 (*                     https://specs.vac.dev/mvds.html                     *)
 (***************************************************************************)
-EXTENDS Naturals, Sequences, TLC
+EXTENDS Naturals, Sequences
 
 CONSTANTS N \* the set of all possible nodes
 

MVDS/Makefile

@@ -0,0 +1,15 @@
+WORKERS := 4
+
+TLA := docker run --rm -it --workdir /mnt -v ${shell pwd}:/mnt talex5/tla
+
+.PHONY: all check tlaps
+
+all: check tlaps
+
+# Run the TLC model checker
+check:
+	${TLA} tlc -workers ${WORKERS} MVDS.tla -config models/SpecOK.cfg
+
+# Run the TLAPS proof checker
+tlaps:
+	${TLA} tlapm -I /usr/local/lib/tlaps MVDS.tla

MVDS/README.md

@@ -4,12 +4,5 @@ TLA+ specification of the [MVDS](https://specs.vac.dev/mvds.html) spec.
 
 ## Model Checking
 
-The model uses 2 nodes who both exchange 1 message.
+- **SpecOK:** This Model runs with 2 validators and uses the `AllMessagesDelivered` state constraint. It proves that messages are eventually received by peers if requested.
 
-State constraint:
-
-```tla
-AllMessagesDelivered
-```
-
-The model checker generates 33 distinct states.

MVDS/models/SpecOK.cfg

@@ -0,0 +1,8 @@
+CONSTANT N = 2
+
+CONSTRAINT AllMessagesDelivered
+
+INVARIANT TypeOK
+
+SPECIFICATION
+Spec

Makefile

@@ -0,0 +1,3 @@
+all:
+	$(MAKE) -C MVDS all
+.PHONY: all

README.md

@@ -1,5 +1,8 @@
 # Formalities
 
+[![License](https://img.shields.io/github/license/vacp2p/formalities.svg)](LICENSE)
+[![Build Status](https://travis-ci.com/vacp2p/formalities.svg?branch=master)](https://travis-ci.com/vacp2p/formalities)
+
 This repository contains TLA+ specifications for [vac](https://specs.vac.dev).
 
 The current specs implemented: