| 1 |
50 |
tbourke |
<?xml version='1.0' encoding='utf-8'?><!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_1.dtd'><nta><declaration>/*
|
| 2 |
|
|
description: Elementary channels. Selection bindings/negated guard clash.
|
| 3 |
|
|
(Figure 4, Bourke & Sowmya, EMSOFT'08)
|
| 4 |
|
|
Also tests for typedefed scalar selection bindings.
|
| 5 |
|
|
stderr: urpal:forall bindings (s) are shared across disjuncts: possible split zones
|
| 6 |
|
|
|
| 7 |
52 |
tbourke |
uppaalerror: 1
|
| 8 |
|
|
|
| 9 |
50 |
tbourke |
layout: neato
|
| 10 |
|
|
|
| 11 |
|
|
author: T. Bourke
|
| 12 |
|
|
created: 20071023
|
| 13 |
|
|
*/
|
| 14 |
|
|
|
| 15 |
|
|
const int N=5;
|
| 16 |
|
|
typedef scalar[N] IDXT;
|
| 17 |
|
|
chan c;
|
| 18 |
|
|
</declaration><template><name x="5" y="5">Template</name><declaration>// Place local declarations here.
|
| 19 |
|
|
|
| 20 |
|
|
clock x, y;
|
| 21 |
|
|
|
| 22 |
|
|
int a[IDXT], b[IDXT];
|
| 23 |
|
|
</declaration><location id="id0" x="200" y="-32"></location><location id="id1" x="-40" y="-32"></location><init ref="id1"/><transition><source ref="id1"/><target ref="id0"/><label kind="select" x="-48" y="-128">s:IDXT</label><label kind="guard" x="24" y="-128">x<a[s] && y>b[s]</label><label kind="synchronisation" x="168" y="-128">c?</label><nail x="-40" y="-104"/><nail x="200" y="-104"/></transition></template><system>// Place template instantiations here.
|
| 24 |
|
|
Process = Template();
|
| 25 |
|
|
|
| 26 |
|
|
// List one or more processes to be composed into a system.
|
| 27 |
|
|
system Process;</system></nta>
|