Unterschied von Pan mit oder ohne -a

L4_
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 104
Registriert: 24. Apr 2012 15:44

Unterschied von Pan mit oder ohne -a

Beitrag von L4_ »

Hallo,

beim Verifizieren habe ich immer noch nicht genau den Unterschied mit/ohne -a verstanden.

Beispielsweise hatte ich einen claim untersucht, wo ich beim einfachen ausführen 0 error, bei -a jedoch 1 error bekam (d.h. im never claim gibt es ein acceptence Cycle, d.h. meine claim wurde widerlegt).

Dann hatte ich auch mal einen claim untersucht, wo ich bereits beim einfachen ausführen 1 error bekam und hier nun mit/ohne -a scheinbar keinen Unterschied machte. Zusätzlich gab es auch keinen acceptence cycle in dem never claim, sondern nur ein accept label (also keine endlosschleife wie bei acceptence cycle).

Weiß hierzu jemand näheres?

BTW:
In wie fern ist das für Lab2, Task 6 entscheident?

Danke im Voraus!

VG

dschneid
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 271
Registriert: 14. Dez 2009 00:56

Re: Unterschied von Pan mit oder ohne -a

Beitrag von dschneid »

Ganz grob gesprochen: Ohne -a werden keine LTL-Formeln betrachtet. Das heißt, wenn du diese Flag weglässt, dann können Modelle verifiziert werden obwohl sie eine angegebene LTL-Formel verletzen.

Antworten

Zurück zu „Archiv“