Activity (RSS)

(from [c07efc77da81821cbca65c1df3aba7959bba2e1e]) Interleave now synchronizes on ✓

The ✓ event must always be part of the synchronization alphabet for

any pa...

The ✓ event must always be part of the synchronization alphabet for any parallel composition, including interleaving. The current interleaving implementation ...

(from [b692420844370837a19641f3b29f71bad483b21a]) Adding acceptance sets for LTSs

This patch adds support for acceptance sets in an LTS. Each stable

node in...

This is related to ticket #4 — since what we actually implemented before was “timeout”, we should now go ahead and implement the real “interrupt” operator.

(from [58e5a3a4444fde5983b86b446359223f2ca9d598]) Current “interrupt” operator is actually “timeout”

The operator that's currently called “interrupt” is actua...

The operator that's currently called “interrupt” (▵ ) is actually the timeout operator (▹).

The differences between the two are subtle. In P▹Q, it's an inter...

We need to add support for failures refinement. This will first require adding failures information to the underlying LTSs. It might be desirable to only inc...

A major new subsystem that we need is a compiler from the existing higher-level CSPM language down to the CSP₀ “assembly” language. None of the design decisio...

(from [7c29484dc2c66b9afc90f23782049eacf5e1c6ec]) Adding comments to CSP₀ scripts

This patch adds support for comments in CSP₀ scripts. They use the

same sy...

I'm going to use Perl-style comments. They start at a # character and extend to the end of the current line.

# Just like this!

It would be nice to be able to have comments in a CSP₀ script.