diff --git a/.github/workflows/latex.yml b/.github/workflows/latex.yml new file mode 100644 index 0000000..565fa9a --- /dev/null +++ b/.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 \ No newline at end of file diff --git a/.gitignore b/.gitignore index c31fb60..3b01203 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ +.gradle *.aux *.glo *.gls diff --git a/Makefile b/Makefile deleted file mode 100644 index 49466c3..0000000 --- a/Makefile +++ /dev/null @@ -1,25 +0,0 @@ -default: lstEventB.pdf sample-lstEventB.pdf sample-lstEventB-colour.pdf - -lstEventB.pdf: lstEventB.sty - pdflatex lstEventB.dtx - makeindex -s gglo.ist -o lstEventB.gls lstEventB.glo - makeindex -s gind.ist -o lstEventB.ind lstEventB.idx - pdflatex lstEventB.dtx - -lstEventB.sty: lstEventB.ins lstEventB.dtx - pdflatex lstEventB.ins - -sample-lstEventB.pdf: sample-lstEventB.tex sample-main.tex lstEventB.sty - pdflatex sample-lstEventB.tex - pdflatex sample-lstEventB.tex - -sample-lstEventB-colour.pdf: sample-lstEventB-colour.tex sample-main.tex lstEventB.sty - pdflatex sample-lstEventB-colour.tex - pdflatex sample-lstEventB-colour.tex - -clean: - rm -f *.aux lstEventB.glo lstEventB.gls lstEventB.idx lstEventB.ilg lstEventB.ind *.log lstEventB.toc - -cleanall: clean - rm -f lstEventB.pdf lstEventB.sty sample-lstEventB.pdf sample-lstEventB-colour.pdf - diff --git a/README.md b/README.md index e6b01c9..af8db8c 100644 --- a/README.md +++ b/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 - +-- Copyright (C) 2016, 2021 University of Southampton diff --git a/Sensor_m0_SNSR.bumx b/Sensor_m0_SNSR.bumx index 735f04f..4f94342 100644 --- a/Sensor_m0_SNSR.bumx +++ b/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 \ No newline at end of file diff --git a/Sensor_m1_DEP.bumx b/Sensor_m1_DEP.bumx index 6b66734..80c9816 100644 --- a/Sensor_m1_DEP.bumx +++ b/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 \ No newline at end of file diff --git a/Sensor_m2_Snsr.bumx b/Sensor_m2_Snsr.bumx index 5533374..4fb8798 100644 --- a/Sensor_m2_Snsr.bumx +++ b/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 \ No newline at end of file diff --git a/Sensor_m3_Ctrl.bumx b/Sensor_m3_Ctrl.bumx index b6dcb3b..34b4aa1 100644 --- a/Sensor_m3_Ctrl.bumx +++ b/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 \ No newline at end of file diff --git a/build.gradle b/build.gradle new file mode 100644 index 0000000..72f3462 --- /dev/null +++ b/build.gradle @@ -0,0 +1,136 @@ +/** + * Copyright (C) 2018 Thai Son Hoang + * Gradle script for building LaTeX package. + * + * Contributors + * Thai Son Hoang - Initial API and implementation. + */ + +defaultTasks 'build' + +/** + * Extra Properties: + * - The base name for the main LaTeX file + * - The LaTeX Program + */ +ext { + BASENAME = 'lstEventB' + LATEX = 'pdflatex' + BIBTEX = 'bibtex' + MAKEINDEX = 'makeindex' +} + +/* The project */ +project.ext { + DTXFile = BASENAME + '.dtx' + INSFile = BASENAME + '.ins' + TEXFile = BASENAME + '.tex' + AUXFile = BASENAME + '.aux' + BBLFile = BASENAME + '.bbl' + PDFFile = BASENAME + '.pdf' + STYFile = BASENAME + '.sty' + GLOFile = BASENAME + '.glo' + GLSFile = BASENAME + '.gls' + IDXFile = BASENAME + '.idx' + INDFile = BASENAME + '.ind' + SAMPLE_FILES = ['sample-lstEventB', 'sample-lstEventB-colour'] + SAMPLE_PREFIX = 'sample' + SAMPLE_DELETE_PREFIX = 'deleteSample' +} + +task sty(type: Exec) { + inputs.files INSFile, DTXFile + outputs.file STYFile + + doFirst { + deleteSTYFile() + } + + commandLine LATEX, "$project.INSFile" +} + +void deleteSTYFile() { + exec { + commandLine 'rm', '-f', "$project.STYFile" + } +} + + +task pdf() { + dependsOn sty + inputs.files DTXFile, STYFile + outputs.file PDFFile + doLast{ + pdf_steps() + } +} + +void pdf_steps() { + exec { + commandLine LATEX, "$project.DTXFile" + } + exec { + commandLine MAKEINDEX, '-s', 'gglo.ist', '-o', "$project.GLSFile", "$project.GLOFile" + } + exec { + commandLine MAKEINDEX, '-s', 'gglo.ist', '-o', "$project.INDFile", "$project.IDXFile" + } + exec { + commandLine LATEX, "$project.DTXFile" + } + exec { + commandLine LATEX, "$project.DTXFile" + } +} + +SAMPLE_FILES.each { def sampleFile -> + task "$SAMPLE_PREFIX$sampleFile"() { + dependsOn sty + inputs.files STYFile, sampleFile+".tex", 'sample-main.tex' + outputs.file sampleFile+".pdf" + doLast{ + sample_steps(sampleFile) + } + } +} + +void sample_steps(sampleFile) { + exec { + commandLine LATEX, sampleFile + } + exec { + commandLine LATEX, sampleFile + } +} + +/* + * @TODO: Make the list of generated files a variable + */ +task clean(type: Delete) { + delete fileTree('.').include('**/*.aux'), fileTree('.').include('**/*.glo'), fileTree('.').include('**/*.gls'), fileTree('.').include('**/*.idx'), fileTree('.').include('**/*.ilg'), fileTree('.').include('**/*.ind'), fileTree('.').include('**/*.log'), fileTree('.').include('**/*.out'), fileTree('.').include('**/*.toc'), fileTree('.').include('**/*.rel') +} + +task cleanall(type: Delete) { + dependsOn clean + delete PDFFile, STYFile + dependsOn tasks.matching { + Task task -> task.name.startsWith(SAMPLE_DELETE_PREFIX) + } +} + +SAMPLE_FILES.each {def sampleFile -> + task "$SAMPLE_DELETE_PREFIX$sampleFile"(type: Delete) { + delete sampleFile+".pdf" + } +} + +task build { + dependsOn 'pdf' + dependsOn tasks.matching { + Task task -> task.name.startsWith(SAMPLE_PREFIX) + } +} + +task all { + dependsOn 'build', 'clean' +} \ No newline at end of file diff --git a/docs/index.md b/docs/index.md new file mode 100644 index 0000000..fc3e79b --- /dev/null +++ b/docs/index.md @@ -0,0 +1,2 @@ +## Welcome to lstEventB.sty + diff --git a/gradle/wrapper/gradle-wrapper.jar b/gradle/wrapper/gradle-wrapper.jar new file mode 100755 index 0000000..ccebba7 Binary files /dev/null and b/gradle/wrapper/gradle-wrapper.jar differ diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties new file mode 100644 index 0000000..bdc9a83 --- /dev/null +++ b/gradle/wrapper/gradle-wrapper.properties @@ -0,0 +1,6 @@ +distributionBase=GRADLE_USER_HOME +distributionPath=wrapper/dists +distributionUrl=https\://services.gradle.org/distributions/gradle-8.0.2-bin.zip +networkTimeout=10000 +zipStoreBase=GRADLE_USER_HOME +zipStorePath=wrapper/dists diff --git a/gradlew b/gradlew new file mode 100755 index 0000000..79a61d4 --- /dev/null +++ b/gradlew @@ -0,0 +1,244 @@ +#!/bin/sh + +# +# Copyright © 2015-2021 the original authors. +# +# Licensed under the Apache License, Version 2.0 (the "License"); +# you may not use this file except in compliance with the License. +# You may obtain a copy of the License at +# +# https://www.apache.org/licenses/LICENSE-2.0 +# +# Unless required by applicable law or agreed to in writing, software +# distributed under the License is distributed on an "AS IS" BASIS, +# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +# See the License for the specific language governing permissions and +# limitations under the License. +# + +############################################################################## +# +# Gradle start up script for POSIX generated by Gradle. +# +# Important for running: +# +# (1) You need a POSIX-compliant shell to run this script. If your /bin/sh is +# noncompliant, but you have some other compliant shell such as ksh or +# bash, then to run this script, type that shell name before the whole +# command line, like: +# +# ksh Gradle +# +# Busybox and similar reduced shells will NOT work, because this script +# requires all of these POSIX shell features: +# * functions; +# * expansions «$var», «${var}», «${var:-default}», «${var+SET}», +# «${var#prefix}», «${var%suffix}», and «$( cmd )»; +# * compound commands having a testable exit status, especially «case»; +# * various built-in commands including «command», «set», and «ulimit». +# +# Important for patching: +# +# (2) This script targets any POSIX shell, so it avoids extensions provided +# by Bash, Ksh, etc; in particular arrays are avoided. +# +# The "traditional" practice of packing multiple parameters into a +# space-separated string is a well documented source of bugs and security +# problems, so this is (mostly) avoided, by progressively accumulating +# options in "$@", and eventually passing that to Java. +# +# Where the inherited environment variables (DEFAULT_JVM_OPTS, JAVA_OPTS, +# and GRADLE_OPTS) rely on word-splitting, this is performed explicitly; +# see the in-line comments for details. +# +# There are tweaks for specific operating systems such as AIX, CygWin, +# Darwin, MinGW, and NonStop. +# +# (3) This script is generated from the Groovy template +# https://github.com/gradle/gradle/blob/HEAD/subprojects/plugins/src/main/resources/org/gradle/api/internal/plugins/unixStartScript.txt +# within the Gradle project. +# +# You can find Gradle at https://github.com/gradle/gradle/. +# +############################################################################## + +# Attempt to set APP_HOME + +# Resolve links: $0 may be a link +app_path=$0 + +# Need this for daisy-chained symlinks. +while + APP_HOME=${app_path%"${app_path##*/}"} # leaves a trailing /; empty if no leading path + [ -h "$app_path" ] +do + ls=$( ls -ld "$app_path" ) + link=${ls#*' -> '} + case $link in #( + /*) app_path=$link ;; #( + *) app_path=$APP_HOME$link ;; + esac +done + +# This is normally unused +# shellcheck disable=SC2034 +APP_BASE_NAME=${0##*/} +APP_HOME=$( cd "${APP_HOME:-./}" && pwd -P ) || exit + +# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script. +DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"' + +# Use the maximum available, or set MAX_FD != -1 to use that value. +MAX_FD=maximum + +warn () { + echo "$*" +} >&2 + +die () { + echo + echo "$*" + echo + exit 1 +} >&2 + +# OS specific support (must be 'true' or 'false'). +cygwin=false +msys=false +darwin=false +nonstop=false +case "$( uname )" in #( + CYGWIN* ) cygwin=true ;; #( + Darwin* ) darwin=true ;; #( + MSYS* | MINGW* ) msys=true ;; #( + NONSTOP* ) nonstop=true ;; +esac + +CLASSPATH=$APP_HOME/gradle/wrapper/gradle-wrapper.jar + + +# Determine the Java command to use to start the JVM. +if [ -n "$JAVA_HOME" ] ; then + if [ -x "$JAVA_HOME/jre/sh/java" ] ; then + # IBM's JDK on AIX uses strange locations for the executables + JAVACMD=$JAVA_HOME/jre/sh/java + else + JAVACMD=$JAVA_HOME/bin/java + fi + if [ ! -x "$JAVACMD" ] ; then + die "ERROR: JAVA_HOME is set to an invalid directory: $JAVA_HOME + +Please set the JAVA_HOME variable in your environment to match the +location of your Java installation." + fi +else + JAVACMD=java + which java >/dev/null 2>&1 || die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH. + +Please set the JAVA_HOME variable in your environment to match the +location of your Java installation." +fi + +# Increase the maximum file descriptors if we can. +if ! "$cygwin" && ! "$darwin" && ! "$nonstop" ; then + case $MAX_FD in #( + max*) + # In POSIX sh, ulimit -H is undefined. That's why the result is checked to see if it worked. + # shellcheck disable=SC3045 + MAX_FD=$( ulimit -H -n ) || + warn "Could not query maximum file descriptor limit" + esac + case $MAX_FD in #( + '' | soft) :;; #( + *) + # In POSIX sh, ulimit -n is undefined. That's why the result is checked to see if it worked. + # shellcheck disable=SC3045 + ulimit -n "$MAX_FD" || + warn "Could not set maximum file descriptor limit to $MAX_FD" + esac +fi + +# Collect all arguments for the java command, stacking in reverse order: +# * args from the command line +# * the main class name +# * -classpath +# * -D...appname settings +# * --module-path (only if needed) +# * DEFAULT_JVM_OPTS, JAVA_OPTS, and GRADLE_OPTS environment variables. + +# For Cygwin or MSYS, switch paths to Windows format before running java +if "$cygwin" || "$msys" ; then + APP_HOME=$( cygpath --path --mixed "$APP_HOME" ) + CLASSPATH=$( cygpath --path --mixed "$CLASSPATH" ) + + JAVACMD=$( cygpath --unix "$JAVACMD" ) + + # Now convert the arguments - kludge to limit ourselves to /bin/sh + for arg do + if + case $arg in #( + -*) false ;; # don't mess with options #( + /?*) t=${arg#/} t=/${t%%/*} # looks like a POSIX filepath + [ -e "$t" ] ;; #( + *) false ;; + esac + then + arg=$( cygpath --path --ignore --mixed "$arg" ) + fi + # Roll the args list around exactly as many times as the number of + # args, so each arg winds up back in the position where it started, but + # possibly modified. + # + # NB: a `for` loop captures its iteration list before it begins, so + # changing the positional parameters here affects neither the number of + # iterations, nor the values presented in `arg`. + shift # remove old arg + set -- "$@" "$arg" # push replacement arg + done +fi + +# Collect all arguments for the java command; +# * $DEFAULT_JVM_OPTS, $JAVA_OPTS, and $GRADLE_OPTS can contain fragments of +# shell script including quotes and variable substitutions, so put them in +# double quotes to make sure that they get re-expanded; and +# * put everything else in single quotes, so that it's not re-expanded. + +set -- \ + "-Dorg.gradle.appname=$APP_BASE_NAME" \ + -classpath "$CLASSPATH" \ + org.gradle.wrapper.GradleWrapperMain \ + "$@" + +# Stop when "xargs" is not available. +if ! command -v xargs >/dev/null 2>&1 +then + die "xargs is not available" +fi + +# Use "xargs" to parse quoted args. +# +# With -n1 it outputs one arg per line, with the quotes and backslashes removed. +# +# In Bash we could simply go: +# +# readarray ARGS < <( xargs -n1 <<<"$var" ) && +# set -- "${ARGS[@]}" "$@" +# +# but POSIX shell has neither arrays nor command substitution, so instead we +# post-process each arg (as a line of input to sed) to backslash-escape any +# character that might be a shell metacharacter, then use eval to reverse +# that process (while maintaining the separation between arguments), and wrap +# the whole thing up as a single "set" statement. +# +# This will of course break if any of these variables contains a newline or +# an unmatched quote. +# + +eval "set -- $( + printf '%s\n' "$DEFAULT_JVM_OPTS $JAVA_OPTS $GRADLE_OPTS" | + xargs -n1 | + sed ' s~[^-[:alnum:]+,./:=@_]~\\&~g; ' | + tr '\n' ' ' + )" '"$@"' + +exec "$JAVACMD" "$@" diff --git a/gradlew.bat b/gradlew.bat new file mode 100644 index 0000000..6689b85 --- /dev/null +++ b/gradlew.bat @@ -0,0 +1,92 @@ +@rem +@rem Copyright 2015 the original author or authors. +@rem +@rem Licensed under the Apache License, Version 2.0 (the "License"); +@rem you may not use this file except in compliance with the License. +@rem You may obtain a copy of the License at +@rem +@rem https://www.apache.org/licenses/LICENSE-2.0 +@rem +@rem Unless required by applicable law or agreed to in writing, software +@rem distributed under the License is distributed on an "AS IS" BASIS, +@rem WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +@rem See the License for the specific language governing permissions and +@rem limitations under the License. +@rem + +@if "%DEBUG%"=="" @echo off +@rem ########################################################################## +@rem +@rem Gradle startup script for Windows +@rem +@rem ########################################################################## + +@rem Set local scope for the variables with windows NT shell +if "%OS%"=="Windows_NT" setlocal + +set DIRNAME=%~dp0 +if "%DIRNAME%"=="" set DIRNAME=. +@rem This is normally unused +set APP_BASE_NAME=%~n0 +set APP_HOME=%DIRNAME% + +@rem Resolve any "." and ".." in APP_HOME to make it shorter. +for %%i in ("%APP_HOME%") do set APP_HOME=%%~fi + +@rem Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script. +set DEFAULT_JVM_OPTS="-Xmx64m" "-Xms64m" + +@rem Find java.exe +if defined JAVA_HOME goto findJavaFromJavaHome + +set JAVA_EXE=java.exe +%JAVA_EXE% -version >NUL 2>&1 +if %ERRORLEVEL% equ 0 goto execute + +echo. +echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH. +echo. +echo Please set the JAVA_HOME variable in your environment to match the +echo location of your Java installation. + +goto fail + +:findJavaFromJavaHome +set JAVA_HOME=%JAVA_HOME:"=% +set JAVA_EXE=%JAVA_HOME%/bin/java.exe + +if exist "%JAVA_EXE%" goto execute + +echo. +echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME% +echo. +echo Please set the JAVA_HOME variable in your environment to match the +echo location of your Java installation. + +goto fail + +:execute +@rem Setup the command line + +set CLASSPATH=%APP_HOME%\gradle\wrapper\gradle-wrapper.jar + + +@rem Execute Gradle +"%JAVA_EXE%" %DEFAULT_JVM_OPTS% %JAVA_OPTS% %GRADLE_OPTS% "-Dorg.gradle.appname=%APP_BASE_NAME%" -classpath "%CLASSPATH%" org.gradle.wrapper.GradleWrapperMain %* + +:end +@rem End local scope for the variables with windows NT shell +if %ERRORLEVEL% equ 0 goto mainEnd + +:fail +rem Set variable GRADLE_EXIT_CONSOLE if you need the _script_ return code instead of +rem the _cmd.exe /c_ return code! +set EXIT_CODE=%ERRORLEVEL% +if %EXIT_CODE% equ 0 set EXIT_CODE=1 +if not ""=="%GRADLE_EXIT_CONSOLE%" exit %EXIT_CODE% +exit /b %EXIT_CODE% + +:mainEnd +if "%OS%"=="Windows_NT" endlocal + +:omega diff --git a/lstEventB.dtx b/lstEventB.dtx index 043028f..0da1b03 100644 --- a/lstEventB.dtx +++ b/lstEventB.dtx @@ -2,23 +2,24 @@ % % lstEventB.ins % -% Copyright (C) 2017 by Thai Son Hoang and Chenyang Zhu -% +% Copyright (C) 2016, 2021 University of Southampton +% % -------------------------------------------------------------------- % % This file may be distributed and/or modified under the -% conditions of the LaTeX Project Public License, either version 1.3 +% conditions of 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 and C. Zhu +% (). % % This work consists of the files lstEventB.dtx, lstEventB.ins, % the derived file lstEventB.sty, the generated documentation @@ -29,11 +30,12 @@ % \iffalse %\NeedsTeXFormat{LaTeX2e}\relax %\ProvidesPackage{lstEventB} -% [2017/08/10 v0.1 Package for listing Event-B code] +% [2020/03/28 v1.1 Package for listing Event-B code] % %<*driver> \documentclass[a4paper]{ltxdoc} -\usepackage{lstEventB} +\usepackage[utf8]{inputenc} +\usepackage[colour]{lstEventB} \EnableCrossrefs % ^^A\CodelineIndex \PageIndex @@ -45,7 +47,7 @@ % % \fi % -% \CheckSum{0} +% \CheckSum{343} % % \CharacterTable % {Upper-case \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z @@ -65,6 +67,10 @@ % % % \changes{v0.1}{2016/08/10}{Initial version} +% \changes{v0.2}{2018/05/14}{Added support for ASCII combinations (Issue \#3)} +% \changes{v1.1}{2020/03/28}{Declare Unicode symbols} +% \changes{v1.1}{2020/03/28}{Fixed symbols for inverse relation, +% multiplication, not subset and not strict subset} % % \GetFileInfo{lstEventB.sty} % @@ -93,7 +99,7 @@ % corresponds to \textsf{lstEventB}~\fileversion, dated~\filedate.}} % \author{Thai Son Hoang and Chenyang Zhu\\ ECS, University of Southampton \\ \texttt{<\{T dot S dot Hoang, C dot Zhu\} at ecs dot % soton dot ac dot uk>}} -% \date{June 6, 2017} +% \date{March 28, 2021} % % \maketitle % @@ -114,15 +120,91 @@ % % ^^A %%%%% Usage %%%%%% % \section{Usage} +% \label{sec:usage} % % Just like any other package, you need to request this package with a -% |\usepackage| command in the preamble. So in the simpler case +% \verb|\usepackage| command in the preamble. So in the simpler case % (i.e., without any options), one just types % % \indent |\usepackage{lstEventB}| % % \noindent to load the package. % +% \subsection{Package Options} +% \label{sec:package-options-usage} +% +% \paragraph{Colouring Option.} +% Loading package with the \verb|colour| or \verb|color| options will enable the +% various colouring of the Event-B code. +% +% \subsection{Typesetting \EventB Code} +% \label{sec:types-eventb-code} +% +% The current supported syntax are from CamilleX (cite XEvent-B paper). In particular, the +% \EventB mathematical symbols can be typeset using Unicode symbols. +% Alternatively, the mathematical symbols can be typeset using ASCII +% combinations (similar to the \EventB Summary (cite Ken Robinson)), +% with the exception that the \emph{text} combinations must be prefixed +% by |!| (this is to prevent unintended translation of text in longer words). Some +% other symbols, e.g. |.| and \verb$|$ also need to be |!|-prefixed. +% +% Table~\ref{tab:predicates} shows the ASCII input for typesetting +% predicate-related symbols. +% \begin{EventBNoShortInline} +% \begin{table}[!htbp] +% \centering +% \begin{tabular}{|l|l|l|} +% \hline +% ASCII & Symbols & Explanation \\ +% \hline +% \verb$!false$ & \lstinline$!false$ & False \\ +% \verb$!true$ & \lstinline$!true$ & True \\ +% \verb$&$ & \lstinline$&$ & Conjunction \\ +% \verb$!or$ & \lstinline$!or$ & Disjunction \\ +% \verb$=>$ & \lstinline$=>$ & Implication \\ +% \verb$<=>$ & \lstinline$<=>$ & Equivalence \\ +% \verb$!not$ & \lstinline$!not$ & Negation \\ +% \verb$!$ & \lstinline$!$ & Universal quantification \\ +% \verb$#$ & \lstinline$#$ & Existential quantification \\ +% \verb$!.$ & \lstinline$.$ & Quantification dot \\ +% \verb$=$ & \lstinline$=$ & Equality \\ +% \verb$/=$ & \lstinline$/=$ & Inequality \\ +% \hline +% \end{tabular} +% \caption{Predicates} +% \label{tab:predicates} +% \end{table} +% \end{EventBNoShortInline} +% +% Table~\ref{tab:sets} shows the ASCII inputs for typesetting +% set-related symbols. +% \begin{EventBNoShortInline} +% \begin{table}[!htbp] +% \centering +% \begin{tabular}{|l|l|l|} +% \hline +% ASCII & Symbols & Explanation \\ +% \hline +% \verb${}$ & \lstinline${}$ & Empty set \\ +% \verb$|$ & \lstinline$|$ & Vertical bar, e.g., in set comprehension \\ +% \verb$\/$ & \lstinline$\/$ & Union \\ +% \verb$/\$ & \lstinline$/\$ & Intersection \\ +% \verb$\$ & \lstinline$\$ & Set difference \\ +% \verb$|->$ & \lstinline$|->$ & Ordered pair \\ +% \verb$**$ & \lstinline$**$ & Cartesian product \\ +% \verb$!POW$ & \lstinline$!POW$ & Powerset \\ +% \verb$!POW1$ & \lstinline$!POW1$ & Non-empty subsets \\ +% \verb$!card$ & \lstinline$!card$ & Cardinality \\ +% \verb$!union$ & \lstinline$!union$ & Generalised union \\ +% \verb$!inter$ & \lstinline$!inter$ & Generalised intersection \\ +% \verb$!UNION$ & \lstinline$!UNION$ & Quantified union \\ +% \verb$!INTER$ & \lstinline$!INTER$ & Quantified intersection \\ +% \hline +% \end{tabular} +% \caption{Sets} +% \label{tab:sets} +% \end{table} +% \end{EventBNoShortInline} % \StopEventually{ % \PrintChanges % \PrintIndex @@ -134,7 +216,7 @@ % ^^A %%% Package loading %%% % Our implementation is based on the |listings| package. % Additionally, we also require |xspace| for spacing, |xcolor| for -% colouring, |bsymb| for typesetting \eventB mathematical symbols, and +% colouring, |bsymb| for typesetting \EventB mathematical symbols, and % |xargs| for defining commands with argument lists. % % \iffalse ^^A BEGIN Produce comments only in the resulting style file @@ -148,6 +230,60 @@ \RequirePackage{xcolor} \RequirePackage{bsymb} \RequirePackage{xargs} +\RequirePackage{mdframed} +\DeclareUnicodeCharacter{22A5}{$\bfalse$} +\DeclareUnicodeCharacter{22A4}{$\btrue$} +\DeclareUnicodeCharacter{2227}{$\land$} +\DeclareUnicodeCharacter{2228}{$\lor$} +\DeclareUnicodeCharacter{21D2}{$\limp$} +\DeclareUnicodeCharacter{21D4}{$\leqv$} +\DeclareUnicodeCharacter{2200}{$\forall$} +\DeclareUnicodeCharacter{2203}{$\exists$} +\DeclareUnicodeCharacter{2260}{$\neq$} +\DeclareUnicodeCharacter{2205}{$\emptyset$} +\DeclareUnicodeCharacter{2223}{$\mid$} +\DeclareUnicodeCharacter{222A}{$\bunion$} +\DeclareUnicodeCharacter{2229}{$\binter$} +\DeclareUnicodeCharacter{2216}{$\setminus$} +\DeclareUnicodeCharacter{21A6}{$\mapsto$} +\DeclareUnicodeCharacter{2119}{$\pow$} +\DeclareUnicodeCharacter{22C3}{$\Union$} +\DeclareUnicodeCharacter{22C2}{$\Inter$} +\DeclareUnicodeCharacter{2208}{$\in$} +\DeclareUnicodeCharacter{2209}{$\notin$} +\DeclareUnicodeCharacter{2286}{$\subseteq$} +\DeclareUnicodeCharacter{2288}{$\not\subseteq$} +\DeclareUnicodeCharacter{2282}{$\subset$} +\DeclareUnicodeCharacter{2284}{$\not\subset$} +\DeclareUnicodeCharacter{2124}{$\intg$} +\DeclareUnicodeCharacter{2115}{$\nat$} +\DeclareUnicodeCharacter{2212}{$-$} +\DeclareUnicodeCharacter{2217}{$*$} +\DeclareUnicodeCharacter{2025}{$\upto$} +\DeclareUnicodeCharacter{2265}{$\geq$} +\DeclareUnicodeCharacter{2264}{$\leq$} +\DeclareUnicodeCharacter{2194}{$\rel$} +\DeclareUnicodeCharacter{E100}{$\trel$} +\DeclareUnicodeCharacter{E101}{$\srel$} +\DeclareUnicodeCharacter{E102}{$\strel$} +\DeclareUnicodeCharacter{2218}{$\circ$} +\DeclareUnicodeCharacter{25C1}{$\domres$} +\DeclareUnicodeCharacter{2A64}{$\domsub$} +\DeclareUnicodeCharacter{25B7}{$\ranres$} +\DeclareUnicodeCharacter{2A65}{$\ransub$} +\DeclareUnicodeCharacter{223C}{$\mathtt{\sim}$} +\DeclareUnicodeCharacter{E103}{$\ovl$} +\DeclareUnicodeCharacter{2297}{$\dprod$} +\DeclareUnicodeCharacter{2225}{$\pprod$} +\DeclareUnicodeCharacter{21F8}{$\pfun$} +\DeclareUnicodeCharacter{2914}{$\pinj$} +\DeclareUnicodeCharacter{21A3}{$\tinj$} +\DeclareUnicodeCharacter{2900}{$\psur$} +\DeclareUnicodeCharacter{21A0}{$\tsur$} +\DeclareUnicodeCharacter{2916}{$\tbij$} +\DeclareUnicodeCharacter{03BB}{$\lambda$} +\DeclareUnicodeCharacter{2254}{$\bcmeq$} + % \end{macrocode} % % \iffalse ^^A BEGIN Produce comments only in the resulting style file @@ -158,7 +294,7 @@ % \subsection{Package Options} % \label{sec:options} % -% We define some options for customising the listing of \eventB code. +% We define some options for customising the listing of \EventB code. % \iffalse ^^A BEGIN Produce comments only in the resulting style file %%%%%% BEGIN Declaration of options %%%%% %% ======================== @@ -173,7 +309,7 @@ % % \begin{macro}{EventB@SetKeywordColour} % Command |EventB@SetKeywordColour| is used to set the colour of the -% \eventB keywords, by default, it is set to |black|. +% \EventB keywords, by default, it is set to |black|. % \iffalse ^^A BEGIN Produce comments only in the resulting style file %% Macro to set the colour of the Event-B keywords. %% The default colour is black. @@ -188,7 +324,7 @@ % % \begin{macro}{EventB@SetNdKeywordColour} % Command |EventB@SetNdKeywordColour| is used to set the colour of the -% secondary \eventB keywords, by default, it is set to |black|. +% secondary \EventB keywords, by default, it is set to |black|. % \iffalse ^^A BEGIN Produce comments only in the resulting style file % %% Macro to set the colour of the Event-B secondary keywords. @@ -204,7 +340,7 @@ % % \begin{macro}{EventB@SetIdentifierColour} % Command |EventB@SetIdentifierColour| is used to set the colour of -% \eventB identifiers, by default, it is set to |black|. +% \EventB identifiers, by default, it is set to |black|. % \iffalse ^^A BEGIN Produce comments only in the resulting style file % %% Macro to set the colour of Event-B identifiers. @@ -220,7 +356,7 @@ % % \begin{macro}{EventB@SetCommentColour} % Command |EventB@SetCommentColour| is used to set the colour of -% \eventB comments, by default, it is set to |black|. +% \EventB comments, by default, it is set to |black|. % \iffalse ^^A BEGIN Produce comments only in the resulting style file % %% Macro to set the colour of Event-B comments. @@ -236,7 +372,7 @@ % % \begin{macro}{EventB@SetFormulaColour} % Command |EventB@SetFormulaColour| is used to set the colour of -% \eventB formulae, by default, it is set to |black|. +% \EventB formulae, by default, it is set to |black|. % \iffalse ^^A BEGIN Produce comments only in the resulting style file % %% Macro to set the colour of Event-B formulae. @@ -253,7 +389,7 @@ % We now define the |colour| option and set the different colours % accordingly. The keywords colour (both first primary and secondary % keywords) is |red|. The identifier colour is |purple|. The comment -% colour is |green|. The formula colour is |blue|. +% colour is |green!50!black| (dark green). The formula colour is |blue|. % \iffalse ^^A BEGIN Produce comments only in the resulting style file % %% Declaration of the *colour* option. @@ -263,7 +399,7 @@ \EventB@SetKeywordColour{red} \EventB@SetNdKeywordColour{red} \EventB@SetIdentifierColour{purple} - \EventB@SetCommentColour{green} + \EventB@SetCommentColour{green!50!black} \EventB@SetFormulaColour{blue} } % \end{macrocode} @@ -300,7 +436,7 @@ % % \subsection{Typesetting of the Event-B language} % \label{sec:eventb-language} -% In this section, we define how to typesetting \eventB code. +% In this section, we define how to typesetting \EventB code. % \iffalse ^^A BEGIN Produce comments only in the resulting style file %%%%%% BEGIN Typesetting of the Event-B Language %%%%% %% =================================== @@ -310,15 +446,16 @@ % \subsubsection{Defining the Event-B language} %\label{sec:define-eventb} % -% We first define the \eventB language using |lstdefinelanguage|. +% We first define the \EventB language using |lstdefinelanguage|. % \iffalse ^^A BEGIN Produce comments only in the resulting style file %% Defining the Event-B language % \fi ^^A END Produce comments only in the resulting style file % \begin{macrocode} +\def\lst@visiblespace{\hspace{0.2em}} \lstdefinelanguage{Event-B}{% basicstyle=\rmfamily\footnotesize, % \end{macrocode} -% Subsequently, we define the keywords of \eventB and how to typeset +% Subsequently, we define the keywords of \EventB and how to typeset % them. Note that the keywords are insensitive. % \begin{macrocode} keywords={% @@ -327,18 +464,18 @@ % Keywords for machines machine,sees,refines,variables,invariants,variant,events,% },% - keywordstyle=\color{EventB@keywordcolour}\bf\sffamily,% + keywordstyle=\color{EventB@keywordcolour}\bfseries\sffamily,% sensitive=false, % \end{macrocode} -% We also define the secondary keywords of \eventB and how to typeset them. +% We also define the secondary keywords of \EventB and how to typeset them. % \begin{macrocode} ndkeywords={% % Keywords for events extended,theorem,any,where,when,with,begin,then% },% - ndkeywordstyle=\color{EventB@ndkeywordcolour}\bf\sffamily,% + ndkeywordstyle=\color{EventB@ndkeywordcolour}\bfseries\sffamily,% % \end{macrocode} -% Next, we define how to typeset \eventB identifiers. +% Next, we define how to typeset \EventB identifiers. % \begin{macrocode} identifierstyle=\color{EventB@identifiercolour}\sffamily, % \end{macrocode} @@ -352,65 +489,175 @@ % \begin{macrocode} stringstyle=\color{EventB@formulacolour}\sffamily, string=[b]", - showstringspaces=false, % Do not show the space in formulae + showstringspaces=true, % Do not show the space in formulae % \end{macrocode} -% Finally, we define the \eventB mathematical symbols using the |bsymb| package +% Finally, we define the \EventB mathematical symbols using the |bsymb| package % as follows. % \begin{macrocode} inputencoding=utf8, % Allow UTF-8 input encoding extendedchars=true, % Use extended characters literate= % Event-B mathematical symbols - {⊥}{{$\bfalse$}}1% - {⊤}{{$\btrue$}}1% - {∧}{{$\land$}}1% - {∨}{{$\lor$}}1% - {⇒}{{$\limp$}}1% - {⇔}{{$\leqv$}}1% - {¬}{{$\lnot$}}1% - {∀}{{$\forall$}}1% - {∃}{{$\exists$}}1% - {·}{{$\qdot$}}1% - {≠}{{$\neq$}}1% - {∅}{{$\emptyset$}}1% - {∪}{{$\bunion$}}1% - {∩}{{$\binter$}}1% - {∖}{{$\setminus$}}1% - {↦}{{$\mapsto$ }}1% - {×}{{$\cprod$ }}1% - {ℙ}{{$\pow$ }}1% - {ℙ1}{{$\pown$ }}1% - {∈}{{$\in$}{ }}2% - {∉}{{$\notin$ }}1% - {⊆}{{$\subseteq$}}1% - {⊈}{{$\nsubseteq$ }}1% - {⊂}{{$\subset$ }}1% - {⊄}{{$\nsubset$ }}1% - {ℤ}{{$\intg$ }}1% - {ℕ}{{$\nat$}}1% - {ℕ1}{{$\natn$ }}1% - {≥}{{$\geq$ }}1% - {≤}{{$\leq$ }}1% - {↔}{{$\rel$ }}1% - {∘}{{$\circ$ }}1% - {◁}{{$\domres$ }}1% - {⩤}{{$\domsub$}}1% - {▷}{{$\ranres$ }}1% - {⩥}{{$\ransub$ }}1% - {∼}{{$\sim$}}1% - {}{{$\ovl$ }}1% - {⊗}{{$\dprod$ }}1% - {∥}{{$\pprod$ }}1% - {⇸}{{$\pfun$ }}1% - {→}{{$\tfun$}}1% - {⤔}{{$\pinj$ }}1% - {↣}{{$\tinj$ }}1% - {⤀}{{$\psur$ }}1% - {↠}{{$\tsur$ }}1% - {⤖}{{$\tbij$ }}1% - {λ}{{$\lambda$ }}1% - {≔}{{$\bcmeq$}{ }}2% - {:∈}{{$\bcmin$}{ }}2% - {:∣}{{$\bcmsuch$}{ }}2% + % Short sequences should appear before long sequences containing them + % Predicates + {⊥}{{$\bfalse$}}1% False + {⊤}{{$\btrue$}}1% True + {∧}{{$\land$}}1% Conjunction + {∨}{{$\lor$}}1% Disjunction + {⇒}{{$\limp$}}1% Implication + {⇔}{{$\leqv$}}1% Equivalence + {¬}{{$\lnot$}}1% Negation + {∀}{{$\forall$}}1% Universal quantification + {∃}{{$\exists$}}1% Existential quantification + {·}{{$\qdot$}}1% Quantification dot + {=}{{$=$}}1% Equality + {≠}{{$\neq$}}1% Inequality + % Sets + {!}{{$\forall$}}1% Universal quantification (This is moved here from ASCII perdicates) + {∅}{{$\emptyset$}}1% Empty set + {∣}{{$\mid$}}1% Vertical bar, e.g., in set comprehension + {∪}{{$\bunion$}}1% Union + {∩}{{$\binter$}}1% Intersection + {∖}{{$\setminus$}}1% Set difference + {↦}{{$\mapsto$}}1% Ordered pair + {×}{{$\cprod$}}1% Cartesian product + {ℙ}{{$\pow$}}1% Powerset + {ℙ1}{{$\pown$}}1% Non-empty subsets + {!card}{{$\card$}}1% Cardinality + {!union}{{$\union$}}1% Generalised union + {!inter}{{$\inter$}}1% Generalised intersection + {⋃}{{$\Union$}}1% Quantified union + {⋂}{{$\Inter$}}1% Quantified intersection + % Set predicates + {∈}{{$\in$}}1% Set membership + {∉}{{$\notin$}}1% Set non-membership + {⊆}{{$\subseteq$}}1% Subset + {⊈}{{$\not\subseteq$}}1% Not a subset + {⊂}{{$\subset$}}1% Proper subset + {⊄}{{$\not\subset$}}1% Not a proper subset + {!finite}{{$\finite$}}1% Finite set + {!partition}{{$\partition$}}1% Partition + % Bool and bool + {!BOOL}{{$\Bool$}}1% BOOL set + {!TRUE}{{$\True$}}1% TRUE + {!FALSE}{{$\False$}}1% FALSE + {!bool}{{$\bool$}}1% bool predicate set + % Numbers + {ℤ}{{$\intg$}}1% Set of integer numbers + {ℕ}{{$\nat$}}1% Set of natural numbers + {ℕ1}{{$\natn$}}1% Set of positive natural numbers + {!min}{{$\min$}}1% Minimum + {!max}{{$\max$}}1% Maximum + {+}{{$+$}}1% Sum + {−}{{$-$}}1% Difference + {∗}{{$*$}}1% Product + {÷}{{$\div$}}1% Quotient + {!mod}{{$\textrm{mod}$}}1% Remainder + {‥}{{$\upto$}}1% Interval + % Number predicates + {≥}{{$\geq$}}1% Greater or equal + {≤}{{$\leq$}}1% Less or equal + % Relations + {↔}{{$\rel$}}1% Relations + {!dom}{{$\dom$}}1% Domain + {!ran}{{$\ran$}}1% Range + {}{{$\trel$}}1% Total relations + {}{{$\srel$}}1% Surjective relations + {}{{$\strel$}}1% Total surjective relations + {∘}{{$\circ$}}1% Backward composition + {!id}{{$\id$}}1% Identity + {◁}{{$\domres$}}1% Domain restriction + {⩤}{{$\domsub$}}1% Domain subtraction + {▷}{{$\ranres$}}1% Range restriction + {⩥}{{$\ransub$}}1% Range subtraction + {∼}{{$\mathtt{\sim}$}}1% Inverse + {}{{$\ovl$}}1% Overriding + {⊗}{{$\dprod$}}1% Direct product + {∥}{{$\pprod$}}1% Parallel product + {!prj1}{{$\prjone$}}1% First projection + {!prj2}{{$\prjtwo$}}1% Second projection + % Functions + {⇸}{{$\pfun$}}1% Partial functions + {→}{{$\tfun$}}1% Total functions + {⤔}{{$\pinj$}}1% Partial injections + {↣}{{$\tinj$}}1% Total injections + {⤀}{{$\psur$}}1% Partial surjections + {↠}{{$\tsur$}}1% Total surjections + {⤖}{{$\tbij$}}1% Bijections + {λ}{{$\lambda$}}1% Lambda abstraction + % Assignment + {≔}{{$\bcmeq$}}1% Becomes equal to + {:∈}{{$\bcmin$}}1% Choice from a set + {:∣}{{$\bcmsuch$}}1% Choice by predicate + % ASCII Number predicates (This has to be before ASCII Predicates) + {>}{{$>$}}1% Greater + {<}{{$<$}}1% Less + {>=}{{$\geq$}}1% Greater or equal + {<=}{{$\leq$}}1% Less or equal + % ASCII Predicates + {!false}{{$\bfalse$}}1% False + {!true}{{$\btrue$}}1% True + {\&}{{$\land$}}1% Conjunction (note the backslash) + {!or}{{$\lor$}}1% Disjunction + {=>}{{$\limp$}}1% Implication + {<=>}{{$\leqv$}}1% Equivalence + {!not}{{$\lnot$}}1% Negation + {\#}{{$\exists$}}1% Existential quantification (note the backslash) + {!.}{{$\qdot$}}1% Quantification dot + {/=}{{$\neq$}}1% Inequality + % ASCII Sets + {\{\}}{{$\emptyset$}}1% Empty set (note the backslashes) + {\|}{{$\mid$}}1% Vertical bar, e.g., in set comprehension (not the backslash) + {\\}{{$\setminus$}}1% Difference + {\\/}{{$\bunion$}}1% Union + {/\\}{{$\binter$}}1% Intersection + {|->}{{$\mapsto$}}1% Ordered pair + {**}{{$\cprod$}}1% Cartesian product + {!POW}{{$\pow$}}1% Powerset + {!POW1}{{$\pown$}}1% Non-empty subsets + {!UNION}{{$\Union$}}1% Quantified union + % ASCII Set predicates + {/:}{{$\notin$}}1% Set non-membership + {/<:}{{$\not\subseteq$}}1% Not a subset + {/<<:}{{$\not\subset$}}1% Not a proper subset + {<<:}{{$\subset$}}1% Proper subset + {<:}{{$\subseteq$}}1% Subset + {!:}{{$\in$}}1% Set membership + % ASCII Numbers + {!INT}{{$\intg$}}1% Set of integer numbers + {!INTER}{{$\Inter$}}1% Quantified intersection (This is moved here from ASCII Sets) + {!NAT}{{$\nat$}}1% Set of natural numbers + {!NAT1}{{$\natn$}}1% Set of positive natural numbers + {-}{{$-$}}1% Difference + {!*}{{$*$}}1% Product (Note the !) + {!/}{{$\div$}}1% Quotient (Note the !) + {..}{{$\upto$}}1% Interval + % ASCII Relations + {<->}{{$\rel$}}1% Relations + {<<->}{{$\trel$}}1% Total relations + {<->>}{{$\srel$}}1% Surjective relations + {<<->>}{{$\strel$}}1% Total surjective relations + {!circ}{{$\circ$}}1% Backward composition + {<|}{{$\domres$}}1% Domain restriction + {<<|}{{$\domsub$}}1% Domain subtraction + {|>}{{$\ranres$}}1% Range restriction + {|>>}{{$\ransub$}}1% Range subtraction + {~}{{$\mathtt{\sim}$}}1% Inverse + {<+}{{$\ovl$}}1% Overriding + {><}{{$\dprod$}}1% Direct product + {||}{{$\pprod$}}1% Parallel product + % ASCII Functions + {+->}{{$\pfun$}}1% Partial functions + {-->}{{$\tfun$}}1% Total functions + {>+>}{{$\pinj$}}1% Partial injections + {>->}{{$\tinj$}}1% Total injections + {+>>}{{$\psur$}}1% Partial surjections + {->>}{{$\tsur$}}1% Total surjections + {>->>}{{$\tbij$}}1% Bijections + {\%}{{$\lambda$}}1% Lambda abstraction + % ASCII Assignment + {:=}{{$\bcmeq$}}1% Becomes equal to + {::}{{$\bcmin$}}1% Choice from a set + {:|}{{$\bcmsuch$}}1% Choice by predicate , % End of Event-B mathematical symbols } % \end{macrocode} @@ -424,9 +671,10 @@ %% Type setting inline Event-B code using | % \fi ^^A END Produce comments only in the resulting style file % \begin{macrocode} -\lstMakeShortInline[language=Event-B, breaklines=f, basicstyle=\rmfamily\normalsize]| +\lstMakeShortInline% +[language=Event-B, breaklines=f, basicstyle=\rmfamily\normalsize]|% % \end{macrocode} -% We then create a dedicated |EventBcode| environment using |lstnewenvironment|. +% We then create a dedicated \verb|EventBcode| environment using \verb|lstnewenvironment|. % \iffalse ^^A BEGIN Produce comments only in the resulting style file % %% Multi-line Event-B code should be wrapped in EventBcode environment. @@ -434,6 +682,29 @@ % \begin{macrocode} \lstnewenvironment{EventBcode}{\lstset{language=Event-B}}{} % \end{macrocode} +% +% We then create a dedicated \verb|EventBNoInline| environment using \verb|newenvironment|. +% \iffalse ^^A BEGIN Produce comments only in the resulting style file +% +%% Multi-line Event-B code should be wrapped in EventBcode environment. +% \fi ^^A END Produce comments only in the resulting style file +% \begin{macrocode} +\newenvironment{EventBNoShortInline} +{ + % Remove the short-inline + \lstDeleteShortInline| + % Set the language to be Event-B + \lstset{language=Event-B, breaklines=f, basicstyle=\rmfamily\normalsize} +} +{ + % Restore the short inline + \lstMakeShortInline[language=Event-B,breaklines=f,basicstyle=\rmfamily\normalsize]| +} +\newcommand{\EventBInline}[1]{% + \lstinline[language=Event-B, breaklines=f,basicstyle=\rmfamily\normalsize]$#1$ +} +% \end{macrocode} +% % Finally, we set some appearance parameters for display the code. % \begin{macrocode} \lstset{% @@ -447,7 +718,7 @@ breaklines=true, % sets automatic line breaking captionpos=b, % sets the caption-position to top mathescape=false, - showspaces=false, % Do not show spaces + showspaces=true, % Do not show spaces showtabs=false, % Do not show tabs xleftmargin=10pt, framexleftmargin=10pt, @@ -469,9 +740,22 @@ % \iffalse ^^A BEGIN Produce comments only in the resulting style file %%%%%% END Typesetting of the Event-B Language %%%%% % \fi ^^A END Produce comments only in the resulting style file +% +% \iffalse ^^A BEGIN Produce comments only in the resulting style file +%%%%%% BEGIN Public commands %%%%% +% \fi ^^A END Produce comments only in the resulting style file +% \begin{macro}{Event@SetKeywordColour} +% \changes{v1.0}{2018/04/28}{Added} +% \begin{macrocode} +\let\EventBSetKeywordColour\EventB@SetKeywordColour +% \end{macrocode} +% \end{macro} % \begin{macrocode} -\newcommand{\eventB}{Event-B\xspace} +\newcommand{\EventB}{Event-B\xspace} % \end{macrocode} +% \iffalse ^^A BEGIN Produce comments only in the resulting style file +%%%%%% BEGIN Public commands %%%%% +% \fi ^^A END Produce comments only in the resulting style file % % \Finale \endinput \ No newline at end of file diff --git a/lstEventB.ins b/lstEventB.ins index eaaff06..6aa0305 100644 --- a/lstEventB.ins +++ b/lstEventB.ins @@ -1,26 +1,26 @@ %% abbrev.ins %% -%% Copyright (C) 2017 by Thai Son Hoang and Chenyang Zhu -%% +%% Copyright (C) 2018 University of Southampton %% -------------------------------------------------------------------- %% %% This file may be distributed and/or modified under the -%% conditions of the LaTeX Project Public License, either version 1.3 +%% conditions of 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 and C. Zhu +%% (). %% %% This work consists of the files lstEventB.dtx, lstEventB.ins, %% the derived file lstEventB.sty, the generated documentation -%% lstEventB.pdf, and some sample requirements documents. +%% lstEventB.pdf, and some sample files. %% \input docstrip.tex @@ -32,22 +32,22 @@ This is a generated file. -Copyright (C) 2017 by Thai Son Hoang and Chenyang Zhu - +Copyright (C) 2018 University of Southampton This file may be distributed and/or modified under the -conditions of the LaTeX Project Public License, either version 1.3 +conditions of 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 and C. Zhu +(). \endpreamble diff --git a/lstEventB.pdf b/lstEventB.pdf index cf3982a..b8c760f 100644 Binary files a/lstEventB.pdf and b/lstEventB.pdf differ diff --git a/lstEventB.sty b/lstEventB.sty index 4106d6f..b4d3928 100644 --- a/lstEventB.sty +++ b/lstEventB.sty @@ -8,26 +8,26 @@ %% %% This is a generated file. %% -%% Copyright (C) 2017 by Thai Son Hoang and Chenyang Zhu -%% +%% Copyright (C) 2018 University of Southampton %% %% This file may be distributed and/or modified under the -%% conditions of the LaTeX Project Public License, either version 1.3 +%% conditions of 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 and C. Zhu +%% (). %% \NeedsTeXFormat{LaTeX2e}\relax \ProvidesPackage{lstEventB} - [2017/08/10 v0.1 Package for listing Event-B code] + [2020/03/28 v1.1 Package for listing Event-B code] %%%%% BEGIN Package loading %%%%% \RequirePackage{listings} @@ -35,6 +35,60 @@ \RequirePackage{xcolor} \RequirePackage{bsymb} \RequirePackage{xargs} +\RequirePackage{mdframed} +\DeclareUnicodeCharacter{22A5}{$\bfalse$} +\DeclareUnicodeCharacter{22A4}{$\btrue$} +\DeclareUnicodeCharacter{2227}{$\land$} +\DeclareUnicodeCharacter{2228}{$\lor$} +\DeclareUnicodeCharacter{21D2}{$\limp$} +\DeclareUnicodeCharacter{21D4}{$\leqv$} +\DeclareUnicodeCharacter{2200}{$\forall$} +\DeclareUnicodeCharacter{2203}{$\exists$} +\DeclareUnicodeCharacter{2260}{$\neq$} +\DeclareUnicodeCharacter{2205}{$\emptyset$} +\DeclareUnicodeCharacter{2223}{$\mid$} +\DeclareUnicodeCharacter{222A}{$\bunion$} +\DeclareUnicodeCharacter{2229}{$\binter$} +\DeclareUnicodeCharacter{2216}{$\setminus$} +\DeclareUnicodeCharacter{21A6}{$\mapsto$} +\DeclareUnicodeCharacter{2119}{$\pow$} +\DeclareUnicodeCharacter{22C3}{$\Union$} +\DeclareUnicodeCharacter{22C2}{$\Inter$} +\DeclareUnicodeCharacter{2208}{$\in$} +\DeclareUnicodeCharacter{2209}{$\notin$} +\DeclareUnicodeCharacter{2286}{$\subseteq$} +\DeclareUnicodeCharacter{2288}{$\not\subseteq$} +\DeclareUnicodeCharacter{2282}{$\subset$} +\DeclareUnicodeCharacter{2284}{$\not\subset$} +\DeclareUnicodeCharacter{2124}{$\intg$} +\DeclareUnicodeCharacter{2115}{$\nat$} +\DeclareUnicodeCharacter{2212}{$-$} +\DeclareUnicodeCharacter{2217}{$*$} +\DeclareUnicodeCharacter{2025}{$\upto$} +\DeclareUnicodeCharacter{2265}{$\geq$} +\DeclareUnicodeCharacter{2264}{$\leq$} +\DeclareUnicodeCharacter{2194}{$\rel$} +\DeclareUnicodeCharacter{E100}{$\trel$} +\DeclareUnicodeCharacter{E101}{$\srel$} +\DeclareUnicodeCharacter{E102}{$\strel$} +\DeclareUnicodeCharacter{2218}{$\circ$} +\DeclareUnicodeCharacter{25C1}{$\domres$} +\DeclareUnicodeCharacter{2A64}{$\domsub$} +\DeclareUnicodeCharacter{25B7}{$\ranres$} +\DeclareUnicodeCharacter{2A65}{$\ransub$} +\DeclareUnicodeCharacter{223C}{$\mathtt{\sim}$} +\DeclareUnicodeCharacter{E103}{$\ovl$} +\DeclareUnicodeCharacter{2297}{$\dprod$} +\DeclareUnicodeCharacter{2225}{$\pprod$} +\DeclareUnicodeCharacter{21F8}{$\pfun$} +\DeclareUnicodeCharacter{2914}{$\pinj$} +\DeclareUnicodeCharacter{21A3}{$\tinj$} +\DeclareUnicodeCharacter{2900}{$\psur$} +\DeclareUnicodeCharacter{21A0}{$\tsur$} +\DeclareUnicodeCharacter{2916}{$\tbij$} +\DeclareUnicodeCharacter{03BB}{$\lambda$} +\DeclareUnicodeCharacter{2254}{$\bcmeq$} + %%%%% END Package loading %%%%% %%%%% BEGIN Declaration of options %%%%% @@ -80,7 +134,7 @@ \EventB@SetKeywordColour{red} \EventB@SetNdKeywordColour{red} \EventB@SetIdentifierColour{purple} - \EventB@SetCommentColour{green} + \EventB@SetCommentColour{green!50!black} \EventB@SetFormulaColour{blue} } @@ -99,6 +153,7 @@ % =================================== % Defining the Event-B language +\def\lst@visiblespace{\hspace{0.2em}} \lstdefinelanguage{Event-B}{% basicstyle=\rmfamily\footnotesize, keywords={% @@ -107,82 +162,209 @@ % Keywords for machines machine,sees,refines,variables,invariants,variant,events,% },% - keywordstyle=\color{EventB@keywordcolour}\bf\sffamily,% + keywordstyle=\color{EventB@keywordcolour}\bfseries\sffamily,% sensitive=false, ndkeywords={% % Keywords for events extended,theorem,any,where,when,with,begin,then% },% - ndkeywordstyle=\color{EventB@ndkeywordcolour}\bf\sffamily,% + ndkeywordstyle=\color{EventB@ndkeywordcolour}\bfseries\sffamily,% identifierstyle=\color{EventB@identifiercolour}\sffamily, comment=[l]{//},% morecomment=[s]{/*}{*/},% commentstyle=\color{EventB@commentcolour}\rmfamily,% stringstyle=\color{EventB@formulacolour}\sffamily, string=[b]", - showstringspaces=false, % Do not show the space in formulae + showstringspaces=true, % Do not show the space in formulae inputencoding=utf8, % Allow UTF-8 input encoding extendedchars=true, % Use extended characters literate= % Event-B mathematical symbols - {⊥}{{$\bfalse$}}1% - {⊤}{{$\btrue$}}1% - {∧}{{$\land$}}1% - {∨}{{$\lor$}}1% - {⇒}{{$\limp$}}1% - {⇔}{{$\leqv$}}1% - {¬}{{$\lnot$}}1% - {∀}{{$\forall$}}1% - {∃}{{$\exists$}}1% - {·}{{$\qdot$}}1% - {≠}{{$\neq$}}1% - {∅}{{$\emptyset$}}1% - {∪}{{$\bunion$}}1% - {∩}{{$\binter$}}1% - {∖}{{$\setminus$}}1% - {↦}{{$\mapsto$ }}1% - {×}{{$\cprod$ }}1% - {ℙ}{{$\pow$ }}1% - {ℙ1}{{$\pown$ }}1% - {∈}{{$\in$}{ }}2% - {∉}{{$\notin$ }}1% - {⊆}{{$\subseteq$}}1% - {⊈}{{$\nsubseteq$ }}1% - {⊂}{{$\subset$ }}1% - {⊄}{{$\nsubset$ }}1% - {ℤ}{{$\intg$ }}1% - {ℕ}{{$\nat$}}1% - {ℕ1}{{$\natn$ }}1% - {≥}{{$\geq$ }}1% - {≤}{{$\leq$ }}1% - {↔}{{$\rel$ }}1% - {∘}{{$\circ$ }}1% - {◁}{{$\domres$ }}1% - {⩤}{{$\domsub$}}1% - {▷}{{$\ranres$ }}1% - {⩥}{{$\ransub$ }}1% - {∼}{{$\sim$}}1% - {}{{$\ovl$ }}1% - {⊗}{{$\dprod$ }}1% - {∥}{{$\pprod$ }}1% - {⇸}{{$\pfun$ }}1% - {→}{{$\tfun$}}1% - {⤔}{{$\pinj$ }}1% - {↣}{{$\tinj$ }}1% - {⤀}{{$\psur$ }}1% - {↠}{{$\tsur$ }}1% - {⤖}{{$\tbij$ }}1% - {λ}{{$\lambda$ }}1% - {≔}{{$\bcmeq$}{ }}2% - {:∈}{{$\bcmin$}{ }}2% - {:∣}{{$\bcmsuch$}{ }}2% + % Short sequences should appear before long sequences containing them + % Predicates + {⊥}{{$\bfalse$}}1% False + {⊤}{{$\btrue$}}1% True + {∧}{{$\land$}}1% Conjunction + {∨}{{$\lor$}}1% Disjunction + {⇒}{{$\limp$}}1% Implication + {⇔}{{$\leqv$}}1% Equivalence + {¬}{{$\lnot$}}1% Negation + {∀}{{$\forall$}}1% Universal quantification + {∃}{{$\exists$}}1% Existential quantification + {·}{{$\qdot$}}1% Quantification dot + {=}{{$=$}}1% Equality + {≠}{{$\neq$}}1% Inequality + % Sets + {!}{{$\forall$}}1% Universal quantification (This is moved here from ASCII perdicates) + {∅}{{$\emptyset$}}1% Empty set + {∣}{{$\mid$}}1% Vertical bar, e.g., in set comprehension + {∪}{{$\bunion$}}1% Union + {∩}{{$\binter$}}1% Intersection + {∖}{{$\setminus$}}1% Set difference + {↦}{{$\mapsto$}}1% Ordered pair + {×}{{$\cprod$}}1% Cartesian product + {ℙ}{{$\pow$}}1% Powerset + {ℙ1}{{$\pown$}}1% Non-empty subsets + {!card}{{$\card$}}1% Cardinality + {!union}{{$\union$}}1% Generalised union + {!inter}{{$\inter$}}1% Generalised intersection + {⋃}{{$\Union$}}1% Quantified union + {⋂}{{$\Inter$}}1% Quantified intersection + % Set predicates + {∈}{{$\in$}}1% Set membership + {∉}{{$\notin$}}1% Set non-membership + {⊆}{{$\subseteq$}}1% Subset + {⊈}{{$\not\subseteq$}}1% Not a subset + {⊂}{{$\subset$}}1% Proper subset + {⊄}{{$\not\subset$}}1% Not a proper subset + {!finite}{{$\finite$}}1% Finite set + {!partition}{{$\partition$}}1% Partition + % Bool and bool + {!BOOL}{{$\Bool$}}1% BOOL set + {!TRUE}{{$\True$}}1% TRUE + {!FALSE}{{$\False$}}1% FALSE + {!bool}{{$\bool$}}1% bool predicate set + % Numbers + {ℤ}{{$\intg$}}1% Set of integer numbers + {ℕ}{{$\nat$}}1% Set of natural numbers + {ℕ1}{{$\natn$}}1% Set of positive natural numbers + {!min}{{$\min$}}1% Minimum + {!max}{{$\max$}}1% Maximum + {+}{{$+$}}1% Sum + {−}{{$-$}}1% Difference + {∗}{{$*$}}1% Product + {÷}{{$\div$}}1% Quotient + {!mod}{{$\textrm{mod}$}}1% Remainder + {‥}{{$\upto$}}1% Interval + % Number predicates + {≥}{{$\geq$}}1% Greater or equal + {≤}{{$\leq$}}1% Less or equal + % Relations + {↔}{{$\rel$}}1% Relations + {!dom}{{$\dom$}}1% Domain + {!ran}{{$\ran$}}1% Range + {}{{$\trel$}}1% Total relations + {}{{$\srel$}}1% Surjective relations + {}{{$\strel$}}1% Total surjective relations + {∘}{{$\circ$}}1% Backward composition + {!id}{{$\id$}}1% Identity + {◁}{{$\domres$}}1% Domain restriction + {⩤}{{$\domsub$}}1% Domain subtraction + {▷}{{$\ranres$}}1% Range restriction + {⩥}{{$\ransub$}}1% Range subtraction + {∼}{{$\mathtt{\sim}$}}1% Inverse + {}{{$\ovl$}}1% Overriding + {⊗}{{$\dprod$}}1% Direct product + {∥}{{$\pprod$}}1% Parallel product + {!prj1}{{$\prjone$}}1% First projection + {!prj2}{{$\prjtwo$}}1% Second projection + % Functions + {⇸}{{$\pfun$}}1% Partial functions + {→}{{$\tfun$}}1% Total functions + {⤔}{{$\pinj$}}1% Partial injections + {↣}{{$\tinj$}}1% Total injections + {⤀}{{$\psur$}}1% Partial surjections + {↠}{{$\tsur$}}1% Total surjections + {⤖}{{$\tbij$}}1% Bijections + {λ}{{$\lambda$}}1% Lambda abstraction + % Assignment + {≔}{{$\bcmeq$}}1% Becomes equal to + {:∈}{{$\bcmin$}}1% Choice from a set + {:∣}{{$\bcmsuch$}}1% Choice by predicate + % ASCII Number predicates (This has to be before ASCII Predicates) + {>}{{$>$}}1% Greater + {<}{{$<$}}1% Less + {>=}{{$\geq$}}1% Greater or equal + {<=}{{$\leq$}}1% Less or equal + % ASCII Predicates + {!false}{{$\bfalse$}}1% False + {!true}{{$\btrue$}}1% True + {\&}{{$\land$}}1% Conjunction (note the backslash) + {!or}{{$\lor$}}1% Disjunction + {=>}{{$\limp$}}1% Implication + {<=>}{{$\leqv$}}1% Equivalence + {!not}{{$\lnot$}}1% Negation + {\#}{{$\exists$}}1% Existential quantification (note the backslash) + {!.}{{$\qdot$}}1% Quantification dot + {/=}{{$\neq$}}1% Inequality + % ASCII Sets + {\{\}}{{$\emptyset$}}1% Empty set (note the backslashes) + {\|}{{$\mid$}}1% Vertical bar, e.g., in set comprehension (not the backslash) + {\\}{{$\setminus$}}1% Difference + {\\/}{{$\bunion$}}1% Union + {/\\}{{$\binter$}}1% Intersection + {|->}{{$\mapsto$}}1% Ordered pair + {**}{{$\cprod$}}1% Cartesian product + {!POW}{{$\pow$}}1% Powerset + {!POW1}{{$\pown$}}1% Non-empty subsets + {!UNION}{{$\Union$}}1% Quantified union + % ASCII Set predicates + {/:}{{$\notin$}}1% Set non-membership + {/<:}{{$\not\subseteq$}}1% Not a subset + {/<<:}{{$\not\subset$}}1% Not a proper subset + {<<:}{{$\subset$}}1% Proper subset + {<:}{{$\subseteq$}}1% Subset + {!:}{{$\in$}}1% Set membership + % ASCII Numbers + {!INT}{{$\intg$}}1% Set of integer numbers + {!INTER}{{$\Inter$}}1% Quantified intersection (This is moved here from ASCII Sets) + {!NAT}{{$\nat$}}1% Set of natural numbers + {!NAT1}{{$\natn$}}1% Set of positive natural numbers + {-}{{$-$}}1% Difference + {!*}{{$*$}}1% Product (Note the !) + {!/}{{$\div$}}1% Quotient (Note the !) + {..}{{$\upto$}}1% Interval + % ASCII Relations + {<->}{{$\rel$}}1% Relations + {<<->}{{$\trel$}}1% Total relations + {<->>}{{$\srel$}}1% Surjective relations + {<<->>}{{$\strel$}}1% Total surjective relations + {!circ}{{$\circ$}}1% Backward composition + {<|}{{$\domres$}}1% Domain restriction + {<<|}{{$\domsub$}}1% Domain subtraction + {|>}{{$\ranres$}}1% Range restriction + {|>>}{{$\ransub$}}1% Range subtraction + {~}{{$\mathtt{\sim}$}}1% Inverse + {<+}{{$\ovl$}}1% Overriding + {><}{{$\dprod$}}1% Direct product + {||}{{$\pprod$}}1% Parallel product + % ASCII Functions + {+->}{{$\pfun$}}1% Partial functions + {-->}{{$\tfun$}}1% Total functions + {>+>}{{$\pinj$}}1% Partial injections + {>->}{{$\tinj$}}1% Total injections + {+>>}{{$\psur$}}1% Partial surjections + {->>}{{$\tsur$}}1% Total surjections + {>->>}{{$\tbij$}}1% Bijections + {\%}{{$\lambda$}}1% Lambda abstraction + % ASCII Assignment + {:=}{{$\bcmeq$}}1% Becomes equal to + {::}{{$\bcmin$}}1% Choice from a set + {:|}{{$\bcmsuch$}}1% Choice by predicate , % End of Event-B mathematical symbols } % Type setting inline Event-B code using | -\lstMakeShortInline[language=Event-B, breaklines=f, basicstyle=\rmfamily\normalsize]| +\lstMakeShortInline% +[language=Event-B, breaklines=f, basicstyle=\rmfamily\normalsize]|% % Multi-line Event-B code should be wrapped in EventBcode environment. \lstnewenvironment{EventBcode}{\lstset{language=Event-B}}{} + +% Multi-line Event-B code should be wrapped in EventBcode environment. +\newenvironment{EventBNoShortInline} +{ + % Remove the short-inline + \lstDeleteShortInline| + % Set the language to be Event-B + \lstset{language=Event-B, breaklines=f, basicstyle=\rmfamily\normalsize} +} +{ + % Restore the short inline + \lstMakeShortInline[language=Event-B,breaklines=f,basicstyle=\rmfamily\normalsize]| +} +\newcommand{\EventBInline}[1]{% + \lstinline[language=Event-B, breaklines=f,basicstyle=\rmfamily\normalsize]$#1$ +} \lstset{% columns=fullflexible, % The columns are fully flexible. numberbychapter=false, @@ -194,7 +376,7 @@ breaklines=true, % sets automatic line breaking captionpos=b, % sets the caption-position to top mathescape=false, - showspaces=false, % Do not show spaces + showspaces=true, % Do not show spaces showtabs=false, % Do not show tabs xleftmargin=10pt, framexleftmargin=10pt, @@ -211,7 +393,10 @@ \end{mdframed} } %%%%% END Typesetting of the Event-B Language %%%%% -\newcommand{\eventB}{Event-B\xspace} +%%%%% BEGIN Public commands %%%%% +\let\EventBSetKeywordColour\EventB@SetKeywordColour +\newcommand{\EventB}{Event-B\xspace} +%%%%% BEGIN Public commands %%%%% \endinput %% %% End of file `lstEventB.sty'. diff --git a/sample-lstEventB-colour.pdf b/sample-lstEventB-colour.pdf index 958caa8..eeacea7 100644 Binary files a/sample-lstEventB-colour.pdf and b/sample-lstEventB-colour.pdf differ diff --git a/sample-lstEventB.pdf b/sample-lstEventB.pdf index da01c53..c56b82f 100644 Binary files a/sample-lstEventB.pdf and b/sample-lstEventB.pdf differ diff --git a/sample-lstEventB.tex b/sample-lstEventB.tex index e780ec9..87436ca 100644 --- a/sample-lstEventB.tex +++ b/sample-lstEventB.tex @@ -1,4 +1,5 @@ \documentclass{article} +\usepackage[utf8]{inputenc} \usepackage{lstEventB} \input{sample-main.tex} \ No newline at end of file diff --git a/sample-main.tex b/sample-main.tex index d5a9448..a7f9367 100644 --- a/sample-main.tex +++ b/sample-main.tex @@ -1,46 +1,191 @@ \usepackage{verbatim} \usepackage{mdframed} + \title{A Sample Document\\for the Usages of \textsf{lstEventB} Package} \author{Thai Son Hoang\\ECS, University of Southampton\\\texttt{}} \begin{document} \maketitle -For convenient, we define macro \verb|\eventB| for \eventB. +For convenient, we define macro \verb|\EventB| for \EventB. + +We start first with some inline \EventB code by embedding them using a pair of \verb$|$, for example \verb$|@grd1: SNSR = FALSE|$ gives |@grd1: SNSR = FALSE|. Any \EventB formulae including Unicode symbols will be typeset using the \verb|bsymb| package accordingly. -We start first with some inline \eventB code by embedding them using a pair of \verb$|$, for example \verb$|@grd1: "SNSR = FALSE"|$ gives |@grd1: "SNSR = FALSE"|. Any \eventB formulae including Unicode symbols will be typeset using the \verb|bsymb| package accordingly. +\begin{EventBNoShortInline} + \begin{table}[!htbp] + \centering + \begin{tabular}{|l|l|l|} + \hline + ASCII & Symbols & Explanation \\ + \hline + \verb$!:$ & \lstinline$!:$ & Set membership \\ + \verb$/:$ & \lstinline$/:$ & Set non-membership \\ + \verb$<:$ & \lstinline$<:$ & Subset \\ + \verb$/<:$ & \lstinline$/<:$ & Not a subset \\ + \verb$<<:$ & \lstinline$<<:$ & Proper subset \\ + \verb$/<<:$ & \lstinline$/<<:$ & Not a proper subset \\ + \verb$!finite$ & \lstinline$!finite$ & Finite \\ + \verb$!partition$ & \lstinline$!partition$ & Partition \\ + \hline + \end{tabular} + \caption{Set predicates} + \end{table} + + + \begin{table}[!htbp] + \centering + \begin{tabular}{|l|l|l|} + \hline + ASCII & Symbols & Explanation \\ + \hline + \verb$!BOOL$ & \lstinline$!BOOL$ & BOOL set \\ + \verb$!TRUE$ & \lstinline$!TRUE$ & TRUE \\ + \verb$!FALSE$ & \lstinline$!FALSE$ & FALSE \\ + \verb$!bool$ & \lstinline$!bool$ & bool predicate \\ + \hline + \end{tabular} + \caption{BOOL and bool} + \end{table} + + \begin{table}[!htbp] + \centering + \begin{tabular}{|l|l|l|} + \hline + ASCII & Symbols & Explanation \\ + \hline + \verb$!INT$ & \lstinline$!INT$ & Set of integer numbers \\ + \verb$!NAT$ & \lstinline$!NAT$ & Set of natural numbers \\ + \verb$!NAT1$ & \lstinline$!NAT1$ & Set of positive natural numbers \\ + \verb$!min$ & \lstinline$!min$ & Mininum \\ + \verb$!max$ & \lstinline$!max$ & Maximum \\ + \verb$-$ & \lstinline$-$ & Difference \\ + \verb$*$ & \lstinline$*$ & Product \\ + \verb$!/$ & \lstinline$!/$ & Quotient \\ + \verb$!mod$ & \lstinline$!mod$ & Remainder \\ + \verb$..$ & \lstinline$..$ & Interval \\ + \hline + \end{tabular} + \caption{Numbers} + \end{table} + + \begin{table}[!htbp] + \centering + \begin{tabular}{|l|l|l|} + \hline + ASCII & Symbols & Explanation \\ + \hline + \verb$>$ & \lstinline$>$ & Greater \\ + \verb$<$ & \lstinline$<$ & Less \\ + \verb$>=$ & \lstinline$>=$ & Greater or equal \\ + \verb$<=$ & \lstinline$<=$ & Less or equal \\ + \hline + \end{tabular} + \caption{Number predicates} + \end{table} + + \begin{table}[!htbp] + \centering + \begin{tabular}{|l|l|l|} + \hline + ASCII & Symbols & Explanation \\ + \hline + \verb$<->$ & \lstinline$<->$ & Relations \\ + \verb$!dom$ & \lstinline$!dom$ & Domain \\ + \verb$!ran$ & \lstinline$!ran$ & Range \\ + \verb$<<->$ & \lstinline$<<->$ & Total relations \\ + \verb$<->>$ & \lstinline$<<->$ & Surjective relations \\ + \verb$<<->>$ & \lstinline$<<->>$ & Total surjective relations \\ + \verb$!circ$ & \lstinline$!circ$ & Backward composition \\ + \verb$!id$ & \lstinline$!id$ & Identity \\ + \verb$<|$ & \lstinline$<|$ & Domain restriction \\ + \verb$<<|$ & \lstinline$<<|$ & Domain subtraction \\ + \verb$|>$ & \lstinline$|>$ & Range restriction \\ + \verb$|>>$ & \lstinline$|>>$ & Range subtraction \\ + \verb$~$ & \lstinline$~$ & Inverse \\ + \verb$<+$ & \lstinline$<+$ & Overriding \\ + \verb$><$ & \lstinline$><$ & Direct product \\ + \verb$||$ & \lstinline$||$ & Parallel product \\ + \verb$!prj1$ & \lstinline$!prj1$ & First projection \\ + \verb$!prj2$ & \lstinline$!prj2$ & Second projection \\ + \hline + \end{tabular} + \caption{Relations} + \end{table} + + \begin{table}[!htbp] + \centering + \begin{tabular}{|l|l|l|} + \hline + ASCII & Symbols & Explanation \\ + \hline + \verb$+->$ & \lstinline$+->$ & Partial functions \\ + \verb$-->$ & \lstinline$-->$ & Total functions \\ + \verb$>+>$ & \lstinline$>+>$ & Partial injections \\ + \verb$>->$ & \lstinline$>->$ & Total injections \\ + \verb$+>>$ & \lstinline$+>>$ & Partial surjections \\ + \verb$->>$ & \lstinline$->>$ & Total surjections \\ + \verb$>->>$ & \lstinline$>->>$ & Bijections \\ + \verb$%$ & \lstinline$%$ & Lambda abstraction \\ + \hline + \end{tabular} + \caption{Functions} + \end{table} + + \begin{table}[!htbp] + \centering + \begin{tabular}{|l|l|l|} + \hline + ASCII & Symbols & Explanation \\ + \hline + \verb$:=$ & \lstinline$:=$ & Becomes equal to \\ + \verb$::$ & \lstinline$::$ & Choice from a set \\ + \verb$:|$ & \lstinline$:|$ & Choice by predicate \\ + \hline + \end{tabular} + \caption{Functions} + \end{table} +\end{EventBNoShortInline} -More complete piece of code (including the Unicode symbols) can be typeset using the \verb|EventBcode| environment. Below is the typesetting of an \eventB machine. +More complete piece of code (including the Unicode symbols) can be typeset using the \verb|EventBcode| environment. Below is the typesetting of an \EventB machine. \begin{EventBcode} machine Sensor_m0_SNSR variables SNSR 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 \end{EventBcode} -One can includes external file containing \eventB code using the \verb|\EventBinputlisting| command. For example the following is the result of including the code in the file \verb|Sensor_m1_DEP.bumx| using \verb|\EventBinputlisting{Sensor_m1_DEP.bumx}|. +One can change the different colour options. For example, \verb|\EventBSetKeywordColour{blue!50!black}| will change the keyword colour to dark blue. (This has effects only when +\begin{EventBcode} +machine Sensor_m0_SNSR +variables + SNSR +invariants + theorem @thm0_1: SNSR ∈ BOOL +\end{EventBcode} + +One can includes external file containing \EventB code using the \verb|\EventBinputlisting| command. For example the following is the result of including the code in the file \verb|Sensor_m1_DEP.bumx| using \verb|\EventBinputlisting{Sensor_m1_DEP.bumx}|. \EventBinputlisting{Sensor_m1_DEP.bumx} More specifically, one can specify more details on the inclusion, e.g., the ranges, as the following example\\ diff --git a/settings.gradle b/settings.gradle new file mode 100644 index 0000000..e69de29