Skip to content

Commit

Permalink
chore: move to v0.3.1
Browse files Browse the repository at this point in the history
  • Loading branch information
pascalpoizat committed Jan 21, 2020
1 parent 2c7e2e0 commit 858ddbe
Show file tree
Hide file tree
Showing 5 changed files with 11 additions and 10 deletions.
17 changes: 9 additions & 8 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -29,14 +29,15 @@
- soundness
- message-relaxed soundness

for six different communication semantics:
for seven different communication semantics:

- unordered (bag of messages)
- fifo between each couple of processes (array of queues)
- fifo inbox (input queue at each process where messages are added)
- fifo outbox (output queue at each process where messages are fetched)
- global fifo (unique shared queue)
- RSC (realizable with synchronous communication)
- **Bag** (shared message multiset, no ordering)
- **Fifo all** (shared message queue, ordering *wrt.* emission time)
- **Causal**, (shared message causality structure, ordering *wrt.* message emission causality)
- **Realizable with Synchronous Communication (RSC)** (shared 1-sized message buffer)
- **Fifo pair** (message queue for each couple of processes, ordering *wrt.* emission time)
- **Fifo inbox** (input message queue for each process, ordering *wrt.* emission time)
- **Fifo outbox**, (output message queue for each process, ordering *wrt.* emission time)

**New properties and communication semantics can be easily taken into account** (see Sect. 5, *Extending the verification*).

Expand Down Expand Up @@ -197,7 +198,7 @@ Verification requires that:
- `FBPMN_HOME` is set to the place where the `fbpmn` sources have been installed (see Sect. 2).
- `TLA2TOOLS_HOME` is set to the place where `tla2tools.jar` is installed (see Sect. 1).
- `fbpmn` is found on the command `PATH` (see Sect. 3a/3b).
- (**optional, available for Linux and OSX only**) `fbpmn-check` and `fbpmn-logs2dot` (from the `scripts` directory of the source distribution) are found on the command `PATH`.<br/>
- (**optional, available for Linux and OSX only**) `fbpmn-check` and `fbpmn-logs2*` (from the `scripts` directory of the source distribution) are found on the command `PATH`.<br/>

### Principles

Expand Down
2 changes: 1 addition & 1 deletion app/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@ data RCommand = RQuit -- quit REPL
-- | RSmt Text -- save current graph as SMT

fversion :: Text
fversion = "0.3.0"
fversion = "0.3.1"

toolversion :: Text
toolversion = fversion
Expand Down
Binary file modified bpmn.graffle/data.plist
Binary file not shown.
Binary file modified bpmn.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
2 changes: 1 addition & 1 deletion fbpmn.cabal
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
cabal-version: 1.24
name: fbpmn
version: 0.3.0
version: 0.3.1
description: formal tools for BPMN
synopsis: formal tools for BPMN
homepage: https://github.com/pascalpoizat/fbpmn
Expand Down

0 comments on commit 858ddbe

Please sign in to comment.