s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
3593 Commits
5 Branches
0 Tags
31 MiB
 
 
 
 
 
 
Branch: master
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'master'
${ noResults }
prism-accumulation/prism-examples/firewire
Dave Parker 6f5d45b888
Example fixes re new semantics (result reported for initial state by default) - need more filters. 		15 years ago
..
abst Example fixes re new semantics (result reported for initial state by default) - need more filters. 15 years ago
impl Example fixes re new semantics (result reported for initial state by default) - need more filters. 15 years ago
README.txt README files (PTA examples). 15 years ago

README.txt 

This case study concerns the Tree Identify Protocol of the IEEE 1394 High Performance Serial Bus (called ``FireWire'').

These are MDP models, manually constructed from probabilistic timed automaton (PTA) models,
using the "digital clocks" semantics [KNPS06]. You can also find the PTA models, in the directory ../pta/firewire.

We consider the following probabilistic timed automata models of the root contention part of the 
tree identify protocol, which are based on probabilistic I/O automata models presented in [SV99].

impl: which consists of the parallel composition of two nodes (Node1 and Node2),
      and two communication channels (Wire12 for messages from Node1 to Node2,
      and Wire21 for messages from Node2 to Node1) and corresponds to the 
      system Impl of [SV99]. 

abst: which is represented by a single probabilistic timed automaton and is an abstraction of Impl 
      based on the the probabilistic I/O automaton I1 of [SV99].

For more information, see: http://www.prismmodelchecker.org/casest