Download

EVE Source Code

EVE is also available for download. EVE has been tested on Fedora and Ubuntu OS. To download the code, please follow this link: EVE on GitHub.

Some SRML Code Examples

Infinitely repeated matching pennies. Alice (resp. Bob) holds coin ca (resp. cb). They can flip their coins to either head (signified by the variable being true) or tail (false). This round is repeated inifinitely many times. The goal of Alice (resp. Bob) is to win infintely often, expressed by the LTL formula GF (ca <-> cb) (resp. GF !(ca <-> cb)).

Infinitely repeated matching pennies (CGS). Infinitely repeated matching pennies modelled as Concurrent Game Structure (CGS).

Peer-to-peer network game. As presented in [Toumi et al., 2015]. Here, instead of CTL goals, we use LTL.

Ring-based mutual exclusion algorithm. As presented in [Gutierrez et al., 2017a].

Bisimulation Example 1. Motivating example 1 (Figure 1) presented in [Gutierrez et al., 2017b].

Bisimulation Example 2. Motivating example 2 (Figure 2) presented in [Gutierrez et al., 2017b].