~tapaal-dist-ctl/verifypn/verifypn-dist-ctl

void Reducer::CreateInhibitorPlacesAndTransitions(PetriNet* net, PNMLParser::InhibitorArcList inhibarcs, MarkVal* placeInInhib, MarkVal* transitionInInhib) {

//Initialize

for (size_t i = 0; i < net->numberOfPlaces(); i++) {

placeInInhib[i] = 0;

}

for (size_t i = 0; i < net->numberOfTransitions(); i++) {

transitionInInhib[i] = 0;

}

//Construct the inhibitor places/arcs

PNMLParser::InhibitorArcIter arcIter;

for (arcIter = inhibarcs.begin(); arcIter != inhibarcs.end(); arcIter++) {

size_t place = -1;

//Find place number

for (size_t i = 0; i < net->numberOfPlaces(); i++) {

if (net->placeNames()[i] == arcIter->source) {

place = i;

placeInInhib[place] = arcIter->weight;

break;

}

size_t transition = -1;

//Find place number

for (size_t i = 0; i < net->numberOfTransitions(); i++) {

if (net->transitionNames()[i] == arcIter->target) {

transition = i;

transitionInInhib[transition] = arcIter->weight;

break;

}

assert(place >= 0 && transition >= 0);

}

void Reducer::Print(PetriNet* net, MarkVal* m0, MarkVal* placeInQuery, MarkVal* placeInInhib, MarkVal* transitionInInhib) {

fprintf(stdout, "\nNET INFO:\n");

fprintf(stdout, "Number of places: %i\n", net->numberOfPlaces());

fprintf(stdout, "Number of transitions: %i\n\n", net->numberOfTransitions());

for (int j = 0; j < net->numberOfTransitions(); j++) {

fprintf(stdout, "Transition %d:\n", j);

for (int i = 0; i < net->numberOfPlaces(); i++) {

if (net->inArc(i, j) > 0) fprintf(stdout, " Input place %d with arc-weight %d\n", i, net->inArc(i, j));

}

for (int i = 0; i < net->numberOfPlaces(); i++) {

if (net->outArc(j, i) > 0) fprintf(stdout, " Output place %d with arc-weight %d\n", i, net->outArc(j, i));

}

fprintf(stdout, "\n", j);

}

for (int i = 0; i < net->numberOfPlaces(); i++) {

fprintf(stdout, "Marking at place %d is: %d\n", i, m0[i]);

}

for (int i = 0; i < net->numberOfPlaces(); i++) {

fprintf(stdout, "Query count for place %d is: %d\n", i, placeInQuery[i]);

}

for (int i = 0; i < net->numberOfPlaces(); i++) {

fprintf(stdout, "Inhibitor count for place %d is: %d\n", i, placeInInhib[i]);

}

for (int i = 0; i < net->numberOfTransitions(); i++) {

fprintf(stdout, "Inhibitor count for transition %d is: %d\n", i, transitionInInhib[i]);

}

100

101

bool Reducer::ReducebyRuleA(PetriNet* net, MarkVal* m0, MarkVal* placeInQuery, MarkVal* placeInInhib, MarkVal* transitionInInhib) {

102

// Rule A - find transition t that has exactly one place in pre and post and remove one of the places

103

bool continueReductions = false;

104

for (size_t t = 0; t < net->numberOfTransitions(); t++) {

105

if (transitionInInhib[t] > 0) {

106

continue;

107

} // if t has a connected inhibitor arc, it cannot be removed

108

int pPre = -1;

109

int pPost = -1;

110

bool ok = true;

111

for (size_t p = 0; p < net->numberOfPlaces(); p++) {

112

if (net->inArc(p, t) > 0) {

113

if (pPre >= 0 || net->inArc(p, t) > 1 || placeInQuery[p] > 0 || placeInInhib[p] > 0) {

114

pPre = -1;

115

ok = false;

116

break;

117

}

118

pPre = p;

119

}

120

if (net->outArc(t, p) > 0) {

121

if (pPost >= 0 || net->outArc(t, p) > 1 || placeInQuery[p] > 0 || placeInInhib[p] > 0) {

122

pPost = -1;

123

ok = false;

124

break;

125

}

126

pPost = p;

127

}

128

}

129

if (!ok || pPre < 0 || pPost < 0 || pPre == pPost || (m0[pPre] > 0 && m0[pPost] > 0)) {

130

continue; // continue if we didn't find unique pPre and pPost that are different and at least of them with empty initial marking

131

}

132

// Check that pPre goes only to t and that there is no other transition than t that gives to pPost

133

for (size_t _t = 0; _t < net->numberOfTransitions(); _t++) {

134

if (net->inArc(pPre, _t) > 0 && _t != t) {

135

ok = false;

136

break;

137

}

138

}

139

if (!ok) {

140

continue;

141

}

142

continueReductions = true;

143

_ruleA++;

144

// Remember that if the initial marking has tokens in pPre, we should fire t initially

145

if (m0[pPre] > 0) {

146

std::pair<int, int> element(t, m0[pPre]); // first element is transition id, the second how many times it should fire

147

unfoldTransitionsInit->push_back(element);

148

}

149

// Remember that after any transition putting to pPre, we should fire immediately after that also t

150

for (size_t _t = 0; _t < net->numberOfTransitions(); _t++) {

151

if (net->outArc(_t, pPre) > 0) {

152

std::pair<int, int> element(t, net->outArc(_t, pPre)); // first element is transition id, the second how many times it should fire

153

unfoldTransitions[_t].push_back(element);

154

}

155

}

156

// Remove transition t and the place that has no tokens in m0

157

net->updateinArc(pPre, t, 0);

158

net->updateoutArc(t, pPost, 0);

159

net->skipTransition(t);

160

_removedTransitions++;

161

if (m0[pPre] == 0) { // removing pPre

162

_removedPlaces++;

163

for (size_t _t = 0; _t < net->numberOfTransitions(); _t++) {

164

net->updateoutArc(_t, pPost, net->outArc(_t, pPost) + net->outArc(_t, pPre));

165

net->updateoutArc(_t, pPre, 0);

166

}

167

} else if (m0[pPost] == 0) { // removing pPost

168

_removedPlaces++;

169

for (size_t _t = 0; _t < net->numberOfTransitions(); _t++) {

170

net->updateinArc(pPre, _t, net->inArc(pPost, _t));

171

net->updateoutArc(_t, pPre, net->outArc(_t, pPre) + net->outArc(_t, pPost));

172

net->updateinArc(pPost, _t, 0);

173

net->updateoutArc(_t, pPost, 0);

174

}

175

}

176

} // end of Rule A main for-loop

177

return continueReductions;

178

}

179

180

bool Reducer::ReducebyRuleB(PetriNet* net, MarkVal* m0, MarkVal* placeInQuery, MarkVal* placeInInhib, MarkVal* transitionInInhib) {

181

// Rule B - find place p that has exactly one transition in pre and exactly one in post and remove the place

182

bool continueReductions = false;

183

for (size_t p = 0; p < net->numberOfPlaces(); p++) {

184

if (placeInInhib[p] > 0 || m0[p] > 0) {

185

continue; // if p has inhibitor arc or nonzero initial marking it cannot be removed

186

}

187

int tPre = -1;

188

int tPost = -1;

189

bool ok = true;

190

for (size_t t = 0; t < net->numberOfTransitions(); t++) {

191

if (net->outArc(t, p) > 0) {

192

if (tPre >= 0) {

193

tPre = -1;

194

ok = false;

195

break;

196

}

197

tPre = t;

198

}

199

if (net->inArc(p, t) > 0) {

200

if (tPost >= 0) {

201

tPost = -1;

202

ok = false;

203

break;

204

}

205

tPost = t;

206

}

207

}

208

if (!ok || tPre < 0 || tPost < 0 || tPre == tPost || // no unique and different tPre and tPost found

209

(net->outArc(tPre, p) != net->inArc(p, tPost)) || // incoming and outgoing arcs to p have different weight

210

placeInQuery[p] > 0 || placeInInhib[p] > 0 || // p is part of query or has inhibitor arcs connected

211

m0[p] > 0 || // p is marked in the initial marking

212

transitionInInhib[tPre] > 0 || transitionInInhib[tPost] > 0) // tPre or tPost have inhibitor arcs

213

{

214

continue;

215

}

216

// Check if the output places of tPost do not have any inhibitor arcs connected

217

for (size_t _p = 0; _p < net->numberOfPlaces(); _p++) {

218

if (net->outArc(tPost, _p) > 0 && placeInInhib[_p] > 0) {

219

ok = false;

220

break;

221

}

222

}

223

// Check that there is no other place than p that gives to tPost, tPre can give to other places

224

for (size_t _p = 0; _p < net->numberOfPlaces(); _p++) {

225

if (net->inArc(_p, tPost) > 0 && _p != p) {

226

ok = false;

227

break;

228

}

229

}

230

if (!ok) {

231

continue;

232

}

233

continueReductions = true;

234

_ruleB++;

235

// Remember that after tPre we should always fire also tPost

236

std::pair<int, int> element(tPost, 1); // first element is transition id, second how many times it should fire

237

unfoldTransitions[tPre].push_back(element);

238

// Remove place p

239

net->updateoutArc(tPre, p, 0);

240

net->updateinArc(p, tPost, 0);

241

_removedPlaces++;

242

_removedTransitions++;

243

for (size_t _p = 0; _p < net->numberOfPlaces(); _p++) { // remove tPost

244

net->updateoutArc(tPre, _p, net->outArc(tPre, _p) + net->outArc(tPost, _p));

245

net->updateoutArc(tPost, _p, 0);

246

}

247

net->skipTransition(tPost);

248

} // end of Rule B main for-loop

249

return continueReductions;

250

}

251

252

bool Reducer::ReducebyRuleC(PetriNet* net, MarkVal* m0, MarkVal* placeInQuery, MarkVal* placeInInhib, MarkVal* transitionInInhib) {

253

// Rule C - two transitions that put and take from the same places

254

bool continueReductions = false;

255

bool removePlace[net->numberOfPlaces()]; // remember what places can be removed (one input and one output arc only with same weight)

256

for (size_t p = 0; p < net->numberOfPlaces(); p++) {

257

removePlace[p] = false;

258

int inDegree = -1; // weight of transition giving to p (should be exactly one)

259

int outDegree = -1; // weight of transition taking out of p (should be exactly one and equal to inDegree)

260

bool ok = true;

261

for (size_t t = 0; t < net->numberOfTransitions(); t++) {

262

if (net->outArc(t, p) > 0) {

263

if (inDegree >= 0) {

264

ok = false;

265

break;

266

}

267

inDegree = net->outArc(t, p);

268

}

269

if (net->inArc(p, t) > 0) {

270

if (outDegree >= 0) {

271

ok = false;

272

break;

273

}

274

outDegree = net->inArc(p, t);

275

}

276

}

277

if (ok && inDegree == outDegree && inDegree > 0) {

278

removePlace[p] = true; // place p can be considered for removing

279

}

280

}

281

// remove place p1 if possible

282

for (size_t p1 = 0; p1 < net->numberOfPlaces(); p1++) {

283

for (size_t p2 = 0; p2 < net->numberOfPlaces(); p2++) {

284

if (!removePlace[p1] || !removePlace[p2] || p1 == p2 ||

285

placeInQuery[p1] > 0 || placeInInhib[p1] > 0 || m0[p1] > 0) {

286

continue; // place p1 cannot be removed

287

}

288

bool ok = true;

289

int t1 = -1;

290

int t2 = -1;

291

for (size_t t = 0; t < net->numberOfTransitions(); t++) {

292

if (net->outArc(t, p1) > 0 || net->outArc(t, p2) > 0) {

293

if (net->outArc(t, p1) != net->outArc(t, p2) || (t1 >= 0 && t1 != t)) {

294

ok = false;

295

break;

296

} else {

297

t1 = t;

298

}

299

}

300

if (net->inArc(p1, t) > 0 || net->inArc(p2, t) > 0) {

301

if (net->inArc(p1, t) != net->inArc(p2, t) || (t2 >= 0 && t2 != t)) {

302

ok = false;

303

break;

304

} else {

305

t2 = t;

306

}

307

}

308

}

309

if (!ok || t1 == t2) {

310

continue;

311

}

312

assert(t1 != -1 && t2 != -1);

313

// remove place p1

314

continueReductions = true;

315

_ruleC++;

316

net->updateoutArc(t1, p1, 0);

317

net->updateinArc(p1, t2, 0);

318

removePlace[p1] = false;

319

_removedPlaces++;

320

}

321

}

322

return continueReductions;

323

}

324

325

bool Reducer::ReducebyRuleD(PetriNet* net, MarkVal* m0, MarkVal* placeInQuery, MarkVal* placeInInhib, MarkVal* transitionInInhib) {

326

// Rule D - two transitions with the same pre and post and same inhibitor arcs

327

bool continueReductions = false;

328

for (size_t t1 = 0; t1 < net->numberOfTransitions(); t1++) {

329

for (size_t t2 = 0; t2 < t1; t2++) {

330

if (transitionInInhib[t1] > 0 || transitionInInhib[t2] > 0) {

331

continue; // no reduction can take place if transitions connected to inhibitor arcs

332

}

333

bool ok = false;

334

for (size_t p = 0; p < net->numberOfPlaces(); p++) {

335

if (net->inArc(p, t1) != net->inArc(p, t2) || net->outArc(t1, p) != net->outArc(t2, p)) {

336

ok = false; // different preset or postset

337

break;

338

}

339

if (net->inArc(p, t2) > 0 || net->outArc(t2, p) > 0) {

340

ok = true; // we do no want to remove isolated orphan transitions

341

}

342

}

343

if (!ok) {

344

continue;

345

}

346

// Remove transition t2

347

continueReductions = true;

348

_ruleD++;

349

_removedTransitions++;

350

for (size_t p = 0; p < net->numberOfPlaces(); p++) {

351

net->updateoutArc(t2, p, 0);

352

net->updateinArc(p, t2, 0);

353

}

354

net->skipTransition(t2);

355

}

356

} // end of main for loop for rule D

357

return continueReductions;

358

}

359

360

void Reducer::Reduce(PetriNet* net, MarkVal* m0, MarkVal* placeInQuery, MarkVal* placeInInhib, MarkVal* transitionInInhib, int enablereduction) {

361

if (enablereduction == 1) { // in the aggresive reduction all four rules are used as long as they remove something

362

while ( ReducebyRuleA(net, m0, placeInQuery, placeInInhib, transitionInInhib) ||

363

ReducebyRuleB(net, m0, placeInQuery, placeInInhib, transitionInInhib) ||

364

ReducebyRuleC(net, m0, placeInQuery, placeInInhib, transitionInInhib) ||

365

ReducebyRuleD(net, m0, placeInQuery, placeInInhib, transitionInInhib) ) {

366

}

367

} else if (enablereduction ==2) { // for k-boundedness checking only rules A and D are applicable

368

while ( ReducebyRuleA(net, m0, placeInQuery, placeInInhib, transitionInInhib) ||

369

ReducebyRuleD(net, m0, placeInQuery, placeInInhib, transitionInInhib) ) {

370

}

371

}

372

}

373

374

void Reducer::expandTrace(unsigned int t, std::vector<unsigned int>& trace) {

375

trace.push_back(t);

376

for (unfoldTransitionsType::iterator it = unfoldTransitions[t].begin(); it != unfoldTransitions[t].end(); it++) {

377

for (int i = 1; i <= it->second; i++) {

378

expandTrace(it->first, trace);

379

}

380

}

381

}

382

383

const std::vector<unsigned int> Reducer::NonreducedTrace(PetriNet* net, const std::vector<unsigned int>& trace) {

384

// recover the original net

385

for (int p = 0; p < _nplaces; p++) {

386

for (int t = 0; t < _ntransitions; t++) {

387

net->updateinArc(p, t, _inArc[_nplaces * t + p]);

388

net->updateoutArc(t, p, _outArc[_nplaces * t + p]);

389

}

390

}

391

// compute the expanded (nonreduced) trace)

392

std::vector<unsigned int> nonreducedTrace;

393

394

// first expand the transitions that can be fired from the initial marking

395

for (unfoldTransitionsType::iterator it = unfoldTransitionsInit->begin(); it != unfoldTransitionsInit->end(); it++) {

396

for (int i = 1; i <= it->second; i++) {

397

nonreducedTrace.push_back(it->first);

398

}

399

}

400

// now expand the transitions from the trace

401

for (size_t i = 0; i < trace.size(); i++) {

402

expandTrace(trace[i], nonreducedTrace);

403

}

404

405

return nonreducedTrace; // this makes a copy of the vector, but the slowdown is insignificant

406

}

407

408

409

} //PetriNet namespace

Older »