1

 This file has been generated by cocoSim

2


3


4

 System nodes

5


6


7


8


9

node Junctions5_A__To__Junctions5_Junctions5Junction1286_2_Condition_Action(a_1:real)

10


11

returns (a:real);

12


13


14

var a_2:real;

15


16


17

let

18


19


20


21

a_2

22

= a_1 +1.;

23


24


25

(a)

26

= (a_2);

27


28


29

tel

30


31


32


33


34


35


36

node Junctions5_A__To__Junctions5_Junctions5Junction1286_1_Condition_Action(a_1:real)

37


38

returns (a:real);

39


40


41

var a_2:real;

42


43


44

let

45


46


47


48

a_2

49

= a_1 +10.;

50


51


52

(a)

53

= (a_2);

54


55


56

tel

57


58


59


60


61


62


63


64

node Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action(a_1:real)

65


66

returns (a:real);

67


68


69

var a_2:real;

70


71


72

let

73


74


75


76

a_2

77

= a_1 +1000.;

78


79


80

(a)

81

= (a_2);

82


83


84

tel

85


86


87


88


89


90


91

node Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action(a_1:real)

92


93

returns (a:real);

94


95


96

var a_2:real;

97


98


99

let

100


101


102


103

a_2

104

= a_1 +100.;

105


106


107

(a)

108

= (a_2);

109


110


111

tel

112


113


114


115


116


117


118

 Exit action for state :Junctions5_A

119

node Junctions5_A_ex(a_1:real;

120

idJunctions5_Junctions5_1:int;

121

isInner:bool)

122


123

returns (a:real;

124

idJunctions5_Junctions5:int);

125


126


127

var a_2:real;

128

idJunctions5_Junctions5_2:int;

129


130


131

let

132


133


134


135

a_2

136

= if (not isInner) then a_1 +10000.

137

else a_1;

138


139


140

 set state as inactive

141

idJunctions5_Junctions5_2

142

= if (not isInner) then 0 else idJunctions5_Junctions5_1;

143


144


145

(a, idJunctions5_Junctions5)

146

= (a_2, idJunctions5_Junctions5_1);

147


148


149

tel

150


151


152


153


154


155

 Entry action for state :Junctions5_A

156

node Junctions5_A_en(idJunctions5_Junctions5_1:int;

157

isInner:bool)

158


159

returns (idJunctions5_Junctions5:int);

160


161


162

var idJunctions5_Junctions5_2:int;

163


164


165

let

166


167


168


169

 set state as active

170

idJunctions5_Junctions5_2

171

= 1282;

172


173


174

(idJunctions5_Junctions5)

175

= (idJunctions5_Junctions5_2);

176


177


178

tel

179


180


181


182


183


184


185

 Exit action for state :Junctions5_B

186

node Junctions5_B_ex(a_1:real;

187

idJunctions5_Junctions5_1:int;

188

isInner:bool)

189


190

returns (a:real;

191

idJunctions5_Junctions5:int);

192


193


194

var a_2:real;

195

idJunctions5_Junctions5_2:int;

196


197


198

let

199


200


201


202

a_2

203

= if (not isInner) then 0.

204

else a_1;

205


206


207

 set state as inactive

208

idJunctions5_Junctions5_2

209

= if (not isInner) then 0 else idJunctions5_Junctions5_1;

210


211


212

(a, idJunctions5_Junctions5)

213

= (a_2, idJunctions5_Junctions5_1);

214


215


216

tel

217


218


219


220


221


222

 Entry action for state :Junctions5_B

223

node Junctions5_B_en(idJunctions5_Junctions5_1:int;

224

isInner:bool)

225


226

returns (idJunctions5_Junctions5:int);

227


228


229

var idJunctions5_Junctions5_2:int;

230


231


232

let

233


234


235


236

 set state as active

237

idJunctions5_Junctions5_2

238

= 1283;

239


240


241

(idJunctions5_Junctions5)

242

= (idJunctions5_Junctions5_2);

243


244


245

tel

246


247


248

***************************************************State :Junctions5_Junctions5 Automaton***************************************************

249


250

node Junctions5_Junctions5_node(idJunctions5_Junctions5_1:int;

251

x:int;

252

a_1:real)

253


254

returns (idJunctions5_Junctions5:int;

255

a:real);

256


257


258

let

259


260

automaton junctions5_junctions5

261


262

state POINTJunctions5_Junctions5:

263

unless (idJunctions5_Junctions5_1=0) restart POINT__TO__JUNCTIONS5_A_1

264


265


266


267

unless (idJunctions5_Junctions5_1=1282) and ( x mod 3=1 ) restart JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1

268


269


270


271

unless (idJunctions5_Junctions5_1=1282) and ( x mod 3=0 ) restart JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2

272


273


274


275

unless (idJunctions5_Junctions5_1=1282) restart JUNCTIONS5_A_IDL

276


277

unless (idJunctions5_Junctions5_1=1283) restart JUNCTIONS5_B_IDL

278


279

let

280


281

(idJunctions5_Junctions5, a)

282

= (idJunctions5_Junctions5_1, a_1);

283


284


285

tel

286


287


288


289

state POINT__TO__JUNCTIONS5_A_1:

290


291

var idJunctions5_Junctions5_2:int;

292

let

293


294

 transition trace :

295

POINT__To__Junctions5_A_1

296

(idJunctions5_Junctions5_2)

297

= Junctions5_A_en(idJunctions5_Junctions5_1, false);

298


299


300

(idJunctions5_Junctions5)

301

= (idJunctions5_Junctions5_2);

302


303

add unused variables

304

(a)

305

= (a_1);

306


307


308

tel

309


310

until true restart POINTJunctions5_Junctions5

311


312


313


314

state JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_1:

315


316

var idJunctions5_Junctions5_2, idJunctions5_Junctions5_3:int;

317

a_2, a_3, a_4, a_5:real;

318

let

319


320


321


322


323


324

 transition trace :

325

Junctions5_A__To__Junction1286_1, Junction1286__To__Junction1287_1, Junction1287__To__Junctions5_B_1

326

 condition Action : a+=10

327


328

(a_2)

329

= Junctions5_A__To__Junctions5_Junctions5Junction1286_1_Condition_Action(a_1);

330


331


332

 condition Action : a+=100

333


334

(a_3)

335

=

336

if (( x>=2 )) then

337

Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action(a_2)

338

else (a_2);

339


340


341

 condition Action : a+=1000

342


343

(a_4)

344

=

345

if (( x>=2 ) and ( x>=4 )) then

346

Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action(a_3)

347

else (a_3);

348


349


350

(a_5, idJunctions5_Junctions5_2)

351

=

352

if (( x>=2 ) and ( x>=4 )) then

353

Junctions5_A_ex(a_4, idJunctions5_Junctions5_1, false)

354

else (a_4, idJunctions5_Junctions5_1);

355


356


357

(idJunctions5_Junctions5_3)

358

=

359

if (( x>=2 ) and ( x>=4 )) then

360

Junctions5_B_en(idJunctions5_Junctions5_2, false)

361

else (idJunctions5_Junctions5_2);

362


363


364

(idJunctions5_Junctions5, a)

365

=

366

if (( x>=2 ) and ( x>=4 )) then

367

(idJunctions5_Junctions5_3, a_5)

368

else

369

if (( x>=2 )) then

370

(idJunctions5_Junctions5_1, a_3)

371

else (idJunctions5_Junctions5_1, a_2);

372


373


374

tel

375


376

until true restart POINTJunctions5_Junctions5

377


378


379


380

state JUNCTIONS5_A__TO__JUNCTIONS5_JUNCTIONS5JUNCTION1286_2:

381


382

var idJunctions5_Junctions5_2, idJunctions5_Junctions5_3:int;

383

a_2, a_3, a_4, a_5:real;

384

let

385


386


387


388


389


390

 transition trace :

391

Junctions5_A__To__Junction1286_2, Junction1286__To__Junction1287_1, Junction1287__To__Junctions5_B_1

392

 condition Action : a+=1

393


394

(a_2)

395

= Junctions5_A__To__Junctions5_Junctions5Junction1286_2_Condition_Action(a_1);

396


397


398

 condition Action : a+=100

399


400

(a_3)

401

=

402

if (( x>=2 )) then

403

Junctions5_Junctions5Junction1286__To__Junctions5_Junctions5Junction1287_1_Condition_Action(a_2)

404

else (a_2);

405


406


407

 condition Action : a+=1000

408


409

(a_4)

410

=

411

if (( x>=2 ) and ( x>=4 )) then

412

Junctions5_Junctions5Junction1287__To__Junctions5_B_1_Condition_Action(a_3)

413

else (a_3);

414


415


416

(a_5, idJunctions5_Junctions5_2)

417

=

418

if (( x>=2 ) and ( x>=4 )) then

419

Junctions5_A_ex(a_4, idJunctions5_Junctions5_1, false)

420

else (a_4, idJunctions5_Junctions5_1);

421


422


423

(idJunctions5_Junctions5_3)

424

=

425

if (( x>=2 ) and ( x>=4 )) then

426

Junctions5_B_en(idJunctions5_Junctions5_2, false)

427

else (idJunctions5_Junctions5_2);

428


429


430

(idJunctions5_Junctions5, a)

431

=

432

if (( x>=2 ) and ( x>=4 )) then

433

(idJunctions5_Junctions5_3, a_5)

434

else

435

if (( x>=2 )) then

436

(idJunctions5_Junctions5_1, a_3)

437

else (idJunctions5_Junctions5_1, a_2);

438


439


440

tel

441


442

until true restart POINTJunctions5_Junctions5

443


444


445


446

state JUNCTIONS5_A_IDL:

447


448

let

449


450


451


452

(idJunctions5_Junctions5, a)

453

= (idJunctions5_Junctions5_1, a_1);

454


455


456

tel

457


458

until true restart POINTJunctions5_Junctions5

459


460


461


462

state JUNCTIONS5_B_IDL:

463


464

let

465


466


467


468

(idJunctions5_Junctions5, a)

469

= (idJunctions5_Junctions5_1, a_1);

470


471


472

tel

473


474

until true restart POINTJunctions5_Junctions5

475


476


477


478

tel

479


480


481

***************************************************State :Junctions5_Junctions5 Automaton***************************************************

482


483

node Junctions5_Junctions5(x:int)

484


485

returns (a:real);

486


487


488

var a_1: real;

489


490

idJunctions5_Junctions5, idJunctions5_Junctions5_1: int;

491


492

let

493


494

a_1 = 0.0 > pre a;

495


496

idJunctions5_Junctions5_1 = 0 > pre idJunctions5_Junctions5;

497


498


499


500


501


502

(idJunctions5_Junctions5, a)

503

= Junctions5_Junctions5_node(idJunctions5_Junctions5_1, x, a_1);

504


505


506

unused outputs

507


508


509

tel

510


511


512


513

node Junctions5 (x_1_1 : int)

514

returns (a_1_1 : real);

515

var

516

Junctions5_1_1 : real;

517

i_virtual_local : real;

518

let

519

Junctions5_1_1 = Junctions5_Junctions5(x_1_1);

520

a_1_1 = Junctions5_1_1;

521

i_virtual_local= 0.0 > 1.0;

522

tel

523

