Merge pull request #7 from eventB-Soton/latest

Merge v1.1

.github/workflows/latex.yml

@@ -0,0 +1,34 @@
+
+name: "LaTeX"
+
+on:
+  push:
+    branches: [ "latest", "stable" ]
+  pull_request:
+    # The branches below must be a subset of the branches above
+    branches: [ "latest", "stable" ]
+  schedule:
+    - cron: '37 21 * * 5'
+
+jobs:
+  latex:
+    name: LaTeX
+    runs-on: ubuntu-latest
+    permissions:
+      actions: read
+      contents: read
+      security-events: write
+
+    strategy:
+      fail-fast: false
+
+    steps:
+    - name: Checkout repository
+      uses: actions/checkout@v3
+
+    # Initializes the CodeQL tools for scanning.
+    - name: Initialize CodeQL
+      uses: xu-cheng/texlive-action/full@v1
+      with:
+        run: |
+          ./gradlew build --scan -s

.gitignore

@@ -1,3 +1,4 @@
+.gradle
 *.aux
 *.glo
 *.gls

README.md

@@ -1,29 +1,33 @@
-Macros for Requirements Documents
-=================================
+[![Latest
+Status](https://github.com/eventB-Soton/lstEventB/actions/workflows/latex.yml/badge.svg?branch=latest)](https://github.com/eventB-Soton/lstEventB/actions/workflows/latex.yml/badge.svg)
+
+Listing Event-B models
+======================
 
 This package contains a documented style file for easily listing
 Event-B code in LaTeX.
 
-
 Installation
 ------------
 
 The package is already pre-compiled. However, in the case where it is
-needed for recompiling, a Makefile has been provided. The users
-can simply issue the following command:
+needed for recompiling, a Gradle script has been provided. The users can
+simply issue the following command:
 
-  make
+  ./gradlew (on *nix systems)
+or
+  gradlew.bat (on Windows systems)
 
 This will perform the following:
 - To create the style file "lstEventB.sty"
 - To create the documentation "lstEventB.pdf"
 - To create the sample "sample-lstEventB.pdf"
+- To create the sample "sample-lstEventB-colour.pdf"
 
 The style file "lstEventB.sty" should be copied to some proper location
 for LaTeX to find it later (e.g.,
 "/usr/local/share/texmf/tex/lstEventB.sty").
 
-
 Documentation
 -------------
 
@@ -36,19 +40,22 @@ License
 -------
 
 This file may be distributed and/or modified under the conditions of
-the LaTeX Project Public License, either version 1.3 of this license
+the LaTeX Project Public License, either version 1.3c of this license
 or (at your option) any later version.  The latest version of this
 license is in:
 
    http://www.latex-project.org/lppl.txt
 
-and version 1.3 or later is part of all distributions of LaTeX version
-2005/12/01 or later.
+and version 1.3c or later is part of all distributions of LaTeX version
+2008/05/04 or later.
 
 This work has the LPPL maintenance status `author-maintained'.
 
-The Current Maintainer of this work is T.S. Hoang and C. Zhu.
+The Current Maintainer of this work is
+[T.S.Hoang](mailto:T.S.Hoang@ecs.soton.ac.uk "T dot S dot Hoang at ecs
+dot soton dot ac dot uk")
+
+Past Maintainer of this work are
+[C. Zhu](mailto:C.Zhu@ecs.soton.ac.uk "C dot Zhu at ecs dot soton dot ac dot uk")
 
---
-Copyright (C) 2017 by Thai Son Hoang and Chenyang Zhu
-<T dot S dot Hoang and C dot Zhu at ecs dot soton dot ac dot uk>
+-- Copyright (C) 2016, 2021 University of Southampton

Sensor_m0_SNSR.bumx

@@ -6,27 +6,27 @@ variables
 
 invariants
 
-	@thm0_1: "SNSR ∈ BOOL" theorem
+	theorem @thm0_1: SNSR ∈ BOOL
 
 events
 
 	INITIALISATION
 	begin
-		@act1: "SNSR ≔ FALSE"
+		@act1: SNSR ≔ FALSE
 	end
 
 	SNSR_on
 	when
-		@grd1: "SNSR = FALSE"
+		@grd1: SNSR = FALSE
 	then
-		@act1: "SNSR ≔ TRUE"
+		@act1: SNSR ≔ TRUE
 	end
 
 	SNSR_off
 	when
-		@grd1: "SNSR = TRUE"
+		@grd1: SNSR = TRUE
 	then
-		@act1: "SNSR ≔ FALSE"
+		@act1: SNSR ≔ FALSE
 	end
 
 end

Sensor_m1_DEP.bumx

@@ -4,22 +4,20 @@ variables
 	SNSR
 	DEP
 invariants
-	@inv0_1: "DEP ∈ ℕ"
+	@inv0_1: DEP ∈ ℕ
 events
 
 	INITIALISATION extended
 	begin
-		@act2: "DEP ≔ 0"
+		@act2: DEP ≔ 0
 	end
 
-	SNSR_on extended
-	refines SNSR_on
+	SNSR_on extends SNSR_on
 	end
 
-	SNSR_off extended
-	refines SNSR_off
+	SNSR_off extends SNSR_off
 	begin
-		@act2: "DEP ≔ DEP + 1"
+		@act2: DEP ≔ DEP + 1
 	end
 
 end

Sensor_m2_Snsr.bumx

@@ -13,49 +13,46 @@ variables
 
 invariants
 
-	@inv1_1: "Snsr_01 = TRUE ⇒ SNSR = TRUE"
+	@inv1_1: Snsr_01 = TRUE ⇒ SNSR = TRUE
 
-	@inv1_2: "Snsr_10 = TRUE ⇒ SNSR = FALSE"
+	@inv1_2: Snsr_10 = TRUE ⇒ SNSR = FALSE
 
-	@inv1_3: "Snsr_01 = FALSE ∨ Snsr_10 = FALSE"
+	@inv1_3: Snsr_01 = FALSE ∨ Snsr_10 = FALSE
 
 events
 
-	INITIALISATION extended
-	refines INITIALISATION
+	INITIALISATION extends INITIALISATION
 	begin
-		@act3: "Snsr_01 ≔ FALSE"
-		@act4: "Snsr_10 ≔ FALSE"
+		@act3: Snsr_01 ≔ FALSE
+		@act4: Snsr_10 ≔ FALSE
 	end
 
-	SNSR_on extended
-	refines SNSR_on
+	SNSR_on extends SNSR_on
 	when
-		@grd2: "Snsr_10 = FALSE"
+		@grd2: Snsr_10 = FALSE
 	then
-		@act2: "Snsr_01 ≔ TRUE"
+		@act2: Snsr_01 ≔ TRUE
 	end
 
-	SNSR_off extended
-	refines SNSR_off
+	SNSR_off extends SNSR_off
 	when
-		@grd2: "Snsr_01 = FALSE"
+		@grd2: Snsr_01 = FALSE
 	then
-		@act3: "Snsr_10 ≔ TRUE"
+		@act3: Snsr_10 ≔ TRUE
 	end
 
 	ctrl_Senses_Snsr_01
 	when
-		@grd1: "Snsr_01 = TRUE"
+		@grd1: Snsr_01 = TRUE
 	then
-		@act1: "Snsr_01 ≔ FALSE"
+		@act1: Snsr_01 ≔ FALSE
 	end
 
 	ctrl_Senses_Snsr_10
 	when
-		@grd1: "Snsr_10 = TRUE"
+		@grd1: Snsr_10 = TRUE
 	then
-		@act1: "Snsr_10 ≔ FALSE"
+		@act1: Snsr_10 ≔ FALSE
 	end
 
 end

Sensor_m3_Ctrl.bumx

@@ -25,72 +25,67 @@ variables
 invariants
 
 	@inv2_1:
-	"Snsr_01 = FALSE ∧ Snsr_10 = FALSE ∧ ctrl_snsr_01 = FALSE ∧ ctrl_snsr_10 = FALSE ⇒ ctrl_snsr = SNSR"
+	Snsr_01 = FALSE ∧ Snsr_10 = FALSE ∧ ctrl_snsr_01 = FALSE ∧ ctrl_snsr_10 = FALSE ⇒ ctrl_snsr = SNSR
 
-	@inv2_2: "ctrl_dep ∈ ℕ"
+	@inv2_2: ctrl_dep ∈ ℕ
 
-	@inv2_3: "Snsr_10 = FALSE ∧ ctrl_snsr_10 = FALSE ⇒ ctrl_dep = DEP"
+	@inv2_3: Snsr_10 = FALSE ∧ ctrl_snsr_10 = FALSE ⇒ ctrl_dep = DEP
 
-	@inv2_4: "Snsr_10 = TRUE ∨ ctrl_snsr_10 = TRUE ⇒ ctrl_dep = DEP − 1"
+	@inv2_4: Snsr_10 = TRUE ∨ ctrl_snsr_10 = TRUE ⇒ ctrl_dep = DEP − 1
 
-	@inv2_5: "ctrl_snsr_01 = TRUE ⇒ SNSR = TRUE"
+	@inv2_5: ctrl_snsr_01 = TRUE ⇒ SNSR = TRUE
 
-	@inv2_6: "ctrl_snsr_10 = TRUE ⇒ SNSR = FALSE"
+	@inv2_6: ctrl_snsr_10 = TRUE ⇒ SNSR = FALSE
 
-	@inv2_7: "ctrl_snsr_01 = TRUE ⇒ Snsr_01 = FALSE"
+	@inv2_7: ctrl_snsr_01 = TRUE ⇒ Snsr_01 = FALSE
 
-	@inv2_8: "ctrl_snsr_10 = TRUE ⇒ Snsr_10 = FALSE"
+	@inv2_8: ctrl_snsr_10 = TRUE ⇒ Snsr_10 = FALSE
 
 events
 
-	INITIALISATION extended
-	refines INITIALISATION
+	INITIALISATION extends INITIALISATION
 	begin
-		@act5: "ctrl_snsr ≔ FALSE"
-		@act6: "ctrl_dep ≔ 0"
-		@act7: "ctrl_snsr_01 ≔ FALSE"
-		@act8: "ctrl_snsr_10 ≔ FALSE"
+		@act5: ctrl_snsr ≔ FALSE
+		@act6: ctrl_dep ≔ 0
+		@act7: ctrl_snsr_01 ≔ FALSE
+		@act8: ctrl_snsr_10 ≔ FALSE
 	end
 
-	SNSR_on extended
-	refines SNSR_on
+	SNSR_on extends SNSR_on
 	when
-		@grd3: "ctrl_snsr_10 = FALSE"
+		@grd3: ctrl_snsr_10 = FALSE
 	end
 
-	SNSR_off extended
-	refines SNSR_off
+	SNSR_off extends SNSR_off
 	when
-		@grd3: "ctrl_snsr_01 = FALSE"
+		@grd3: ctrl_snsr_01 = FALSE
 	end
 
-	ctrl_Senses_Snsr_01 extended
-	refines ctrl_Senses_Snsr_01
+	ctrl_Senses_Snsr_01 extends ctrl_Senses_Snsr_01
 	begin
-		@act2: "ctrl_snsr_01 ≔ TRUE"
+		@act2: ctrl_snsr_01 ≔ TRUE
 	end
 
-	ctrl_Senses_Snsr_10 extended
-	refines ctrl_Senses_Snsr_10
+	ctrl_Senses_Snsr_10 extends ctrl_Senses_Snsr_10
 	begin
-		@act2: "ctrl_snsr_10 ≔ TRUE"
+		@act2: ctrl_snsr_10 ≔ TRUE
 	end
 
 	ctrl_on
 	when
-		@grd1: "ctrl_snsr_01 = TRUE"
+		@grd1: ctrl_snsr_01 = TRUE
 	then
-		@act1: "ctrl_snsr_01 ≔ FALSE"
-		@act2: "ctrl_snsr ≔ TRUE"
+		@act1: ctrl_snsr_01 ≔ FALSE
+		@act2: ctrl_snsr ≔ TRUE
 	end
 
 	ctrl_off
 	when
-		@grd1: "ctrl_snsr_10 = TRUE"
+		@grd1: ctrl_snsr_10 = TRUE
 	then
-		@act1: "ctrl_snsr_10 ≔ FALSE"
-		@act2: "ctrl_snsr ≔ FALSE"
-		@act3: "ctrl_dep ≔ ctrl_dep + 1"
+		@act1: ctrl_snsr_10 ≔ FALSE
+		@act2: ctrl_snsr ≔ FALSE
+		@act3: ctrl_dep ≔ ctrl_dep + 1
 	end
 
 end