hklarner/nusmv-a

nusmv-a's Issues

Warnungen durchgehen

Für zum Schluss, wenn alles erstmal steht, denke ich: Beim Kompilieren mit build/cmake und build/make bekomme ich noch ein paar Warnungen angezeigt. Ich würde die ganz am Ende, wenn alles sonst soweit steht, nochmal durchgehen wollen und schauen, wie wir sie beheben können.
Nur damit ich's nicht vergesse, jetzt mal als neues Issue aufgenommen.

Abschlußvortrag

Dachte wir können schon mal ein paar Punkte für die Vorträge sammeln aus denen ihr dann auswählen könnt.

Theoretisches

• kurze Beschreibung model checking: Übergangsgraph, CTL Formel, Anfangszustände
• kurze Beschreibung Decision Diagram und Factored Form

Praktisches

• NuSMV command line option
• CUDD factored form
• Ausgabeformat

Anwendungen

• benchmark: "wie lange rechnet NuSMV für ein Boolsches Netz mit n Variablen?"
• beispiel: basins of attraction für veröffentlichte Boolsche Netze

Der Vortrag soll zwischen 30 und 60 min lang sein. Ihr könnt euch überlegen, ob ihr einen Vortrag gemeinsam macht (würde ich empfehlen) oder jeder einen eigenen. Als Termin schlage ich

• 10.Mai 14:15, oder
• 11.Mai 10:15

vor.

printing a BDD in human readable format

check out if this function BddEnc_print_set_of_states or similar are useful.

starting point is the file
SWP2016/NuSMV-2.6.0/NuSMV/code/nusmv/core/fsm/bdd/BddFsmPrint.c

documentation

of new functions in folder https://github.com/hklarner/NuSMV-a/tree/master/NuSMV-2.6.0/NuSMV/doc/user-man/cmd

Kleinigkeiten

Kleinigkeiten:

• (1) den Namen des Parameters, i.e. "interesting_states", durch "filename" ersetzen
• (2) kein .txt and filename anhängen

Funktion schreiben, die Mc_CheckCTLSpec erweitert

• void Mc_CheckCTLSpec_printResults(NuSMVEnv_ptr env, Prop_ptr prop)
• soll bestehende Mc_CheckCTLSpec erweitern und statt dieser aufgerufen werden, wenn nusmv -a aufgerufen wird
• rausfinden, wo Mc_CheckCTLSpec aufgerufen wird, um dort abzufragen, welche Variante ausgefuehrt werden soll

make Error bei commit 104

Hi
ich kann die aktuelle Version (257f420) nicht kompilieren. Habe build/cmake .. und build/make laufen lassen und bekomme

/home/klarner/SWP2016/github/NuSMV-2.6.0/NuSMV/code/nusmv/core/mc/mcPrint.c: In function ‘try_to_print_this’:
/home/klarner/SWP2016/github/NuSMV-2.6.0/NuSMV/code/nusmv/core/mc/mcPrint.c:96:7: warning: passing argument 1 of ‘free’ discards ‘const’ qualifier from pointer target type [enabled by default]
if( (const char*) NULL != inames[i]) { free( inames[i]); }

als ersten Teil einer längeren Fehlermeldung. Kann das jemand bestätigen?

add NuSMV command line option "-a output.txt" and "-a"

"-a" for "return accepting states"

without filename "-a"

• prints accepting states only

with file filename "-a output.txt"

• prints accepting states and saves accepting states in "output.txt"

problem in the installation of NuSMV-2.6.0 in #make

I was installing the NuSMV-2.6.0 program and after executing the make command, these error lines appear, attached file.

Building C object build-cudd / util / CMakeFiles / CUDD_UTIL_LIB.dir / pipefork.c.o
isue NUSMV.txt

My operating system is: Ubuntu 18.04 64bits
Already execute these commands, I think you can add to the installation manual:

sudo apt-get install flex
sudo apt-get install bison

Thanks

Fehlermeldung: Input file is (null)

Hi noch mal,

ich tendiere gerade dazu die beiden command line options -a und -a_file zu einer einzigen, nämlich -a, zusammenzufassen. Und zwar so:

• -a kann entweder eine Datei erzeugen oder die Ergebnisse als Text ausgeben
• -a benötigt einen parameter filename
• ein bestimmter Wert von filename ist, sozusagen als "cheat", für die Bildschirmausgabe reserviert:
  • falls man filename=print angibt wird der Text ausgegeben und keine Datei erzeugt
  • andernfalls wird kein Text ausgegeben aber dafür in eine Datei geschrieben

Ich glaube dadurch ist die Verwendung einfacher, weil der User weniger Auswahlmöglichkeiten hat. Was denkt ihr? Gibt's dadurch irgendwelche Nachteile?

keine *dot* ausgabe

Habe mich jetzt doch dazu entschlossen die Ausgabe von dot Dateien wieder rauszunehmen, nachdem ich erstens nicht genau weiß, ob die Ausgabe wirklich nützlich sein wird und nachdem zweitens die Ausgabe so wie sie bisher implementiert ist keine korrekte dot Datei erzeugt, sondern stattdessen mehrere _dot_s aneinanderhängt. Die Alternative mehrere dot Dateien mit index im Dateinamen zu erzeugen scheint mir auch nicht das richtige zu sein.

Also: bitte alle dot Ausgaben wieder rückgängig machen.

Woche 6

Hallo Frederike und Sarah,

habe gerade die aktuelle Version heruntergeladen und getestet. Läuft. Wir haben offiziell noch zwei Wochen und noch ein größeres Thema offen:

1) der interaktive Modus (shell)

und ein paar kleinere

2) Dokumentation
3) Ausgabe wie in output_corrected.txt
4) Warnungen durchgehen

und ein optionales

4) benchmark

überlegt euch wer wann an welchem Thema arbeitet. Ich bin von jetzt bis zum Schluß da und helfe mit wo ich kann.

Benchmark

Die Idee ist mit einer Stoppuhr festzuhalten, wie lange NuSMV typischerweise braucht um die Accepting states zu berechnen. Die Erwartung und Vermutung ist, daß die Ausgabe der Accepting States keine nennenswerte CPU Zeit brauch, da das entsprechende BDD ja sowiso berechnet werden muss.

Wie lange NuSMV rechnet hängt erstens von der größe des Netzwerks ab und zweitens von der oder den CTL Formeln.

Welche Netzwerke testet man?

1. Zufällig generierte Netzwerke mit einem Parameter n, der festlegt wieviele Komponenten es gibt (bei raf_network.bnet sind es drei), siehe Benchmark
2. Publizierte Netzwerke, siehe Casestudies

Welche CTL Formeln testet man?

Die einfachste Möglichkeit ist Formeln des Typs EF(x) zu testen, wobei x einen einzelnen Zustand referenziert, für x=110 wäre die Formel also

EF(Erk & Mek & !Raf)

Dabei kann man x auch wieder zufällig generieren.

Für die case studies macht es Sinn eine CTL Formel für einen Attraktor zu generieren. Die Formeln kann ich generieren.

Wie stoppt man die Zeit?

Vielleicht mit dem Linux Befehl time? Siehe http://linux.about.com/library/cmd/blcmdl1_time.htm
Ausgabe sieht zum Beispiel so aus:

$ time NuSMV -r big_network.smv
...
...
system diameter: 1
reachable states: 5.49756e+11 (2^39) out of 5.49756e+11 (2^39)

real    9m13.250s
user    9m6.884s
sys 0m6.256s

Wie präsentiert man die Ergebnisse?

• man könnte die Größe des Netzwerkes, also n, gegen die CPU Zeit t plotten.
• für die case studies könnte man eine Tabelle mit den Zeiten angeben
• für zufällige Ergebnisse könnte man angeben wie lange (wieviele Zeichen) die accepting states Formel ist
• die Zeit kann man einmal mit -a und einmal ohne -a stoppen und vergleichen

Week 7

Hallo,

sieht so aus als gäbe es nur noch drei Punkte:

1. Benchmark
2. Vortrag
3. Warnungen durchgehen

richtig?

typo

In der Datei NuSMV-2.6.0/NuSMV/code/nusmv/core/opt/opt.c in der Zeile

void unset_return_acceptin(OptsHandler_ptr opt)

ist ein Typo ("acceptin" anstatt von "accepting")

Can it also generate accepting states for LTL specifications?

Greetings. I would like to know if the same concept can be applied to work with LTL specifications to obtain the accepting states in the system?

Thank you.
Edmond

cuddGarbageCollect

Keine Ahnung, ob das ein echter bug ist oder nur vorübergehend. Jedenfalls führt

NuSMV -a -dcx big_network.smv

zu folgendem Fehler:

cuddGarbageCollect:
problem in table 1
dead count != deleted
This problem is often due to a missing call to Cudd_Ref
or to an extra call to Cudd_RecursiveDeref.
See the CUDD Programmer's Guide for additional details.Aborted (core dumped)

Ausgabeformate

Der Befehl -a soll folgende Zeilen ausgeben (keine Leerzeilen vorher oder nacher):

Initial States: (Erk & !Mek)
Accepting States: Erk
Initial and Accepting States: (Erk & !Mek)

und zwar nach den anderen print statements, die in Mc_CheckCTLSpec core/mc/mcMc.c sonst noch stehen (zum Beispiel das counterexample). Die Idee ist, daß die Ausgabe so aussieht, wie die anderen NuSMV Ausgaben. Da die ursprüngliche Formel schon angegeben ist, müssen wir die nicht nochmal ausgeben.

Der Befehl -a_file soll eine einzige Datei erzeugen in der füŕ jede CTL specification ein Block mit vier Zeilen steht. Blöcke sind durch einzelne Leerzeilen getrennt. Folgendes Beispiel ist für zwei CTL specifications:

CTLSPEC________AG(Erk)
INIT_____________(Erk & !Mek)
ACCEPTING______Erk
INITACCEPTING__(Erk & !Mek)

CTLSPEC________EF(Erk)
INIT_____________(Erk & !Mek)
ACCEPTING______Erk
INITACCEPTING___FALSE

wobei die underscores "__" durch Leerzeichen ersetzt werden sollen. Die Idee hier ist, daß die Datei leicht weiterverarbeitet werden kann, jede Zeile ist im Grunde ein keyword, value Paar, und die Leerzeichen sollen dafür sorgen, dass die Datei trotzdem gut lesbar ist. Der string, der hinter CTLSPEC stehen soll steckt irgendwo in Prop_print (glaube ich) in core/mc/mcMc.c. Eventuell funktioniert auch Prop_get_expr aus core/prop/Prop.c.

Der Name der Datei, die durch -a_file erzeugt wird soll durch den user angegeben werden, durch einen benötigten parameter. Wie das geht wird in dem docstring von NuSMVCore_add_command_line_option in core/cinit/cinit.h erwähnt. Orientieren kann man sich an der command line option -v vl bei der vl der benötigte paramter ist.

Ansonsten super, was ihr alles geschafft habt! Habe die aktuelle Version eben kompiliert und ausprobiert. Läuft.

Organisation der Funktionen

Hi,

soweit ich sehen kann gibt es zwei Dateien an denen wir arbeiten:

• fsm/bdd/BddFsmPrint.c und
• mc/mcMc.c

und derzeit drei Funktionen:

• BddFsm_print_interesting_states_info
• try_to_print_this
• print_this

Ich würde vorschlagen die drei Funktionen in eine, z.B. BddFsm_print_accepting_states_info zusammenzufassen. Damit bleibt mc/mcMc.c möglichst sauber und die Ausgabe der accepting states entspricht der von z.B. den fair states.

Dokumentation

Die Dokumentation sollte drei Teile enthalten:

• Sourcecode habt ihr ja schon angefangen
• Changelog, kurz aufzählen welche Dateien und Funktionen geändert / erzeugt wurden
• Manual das an einem Beispiel (raf_network.smv?) alle typischen batch und interaktiv Modus Aufrufe kurz (inklusive Ausgabe) zeigt und erklärt

Würde vorschlagen ihr erzeugt dazu "markdown" Dateien im Repository: changelog.md und manual.md

Interactive Shell

Hi, habe gerade von einem der Entwickler bei NuSMV eine Email bekommen:

question: would you consider an extension of NuSMV that only
adds a command for the batch mode and does not add an extension for
the interactive mode?

We definitely prefer the solution where we will also have the command in
the interactive shell. Indeed, once ready for the batch doing it for the
shell should be easy (it would be roughly a matter of wrting the function that
call the same code it is called in the batch.

Da es anscheinend einfach ist unsere Erweiterung auch im interaktiven Modus ausführbar zu machen, nehme ich das mal mit auf.