# Petri Net from Source Code

Málið við hesari gransking, er at verificera okkurt um eitt program, við at gera programmið um til eitt Petri-Net, og so fortelja okkurt um netið.

Líkandi tól:
* JavaPathFinder & Brandera translates Java source code into Promela language which is the input language of SPIN
* Feaver produces Promela from C programs
* VeriSoft

## From Code to Coloured Petri Nets: Modelling Guidelines

http://ceur-ws.org/Vol-851/paper8.pdf

Hendan paper bjóðar ikki eina sjálvirkandi metodu til at gera frumforrit um til petri net. Hendan paper bjóðar einans eina mannagongd til hvussu ein burdi umset frumkotuna.

## Transforming sources to petri nets: a way to analyze execution of parallel programs

https://dl.acm.org/doi/10.5555/1416222.1416240

Tað ein vil spyrja um eitt program kann deilast upp í ymisk perspektivir. Kanska ein vil vita um forriti terminerar, og so er einans umráðandi at kannað kontrol-flow í forritinum. Altso, ein kann gloyma detaljir, og einans hyggja eftir einum tingið at gangin. Hetta ger, so at netið, ikki upplivir state-space-expliosion á sama hátt.

Við einum simplificeraðum perspektivi av programminum, har vit einans hyggja eftir control-flow, so burdi verið lætt at gjørt termination proofs við at hyggja eftir strukturinum av programminum. Tvs. lætt at siga at eitt ávíst program fer at terminera, men onkuntíð ber tað ikki til

Dømir uppá Perpektivir:
* Control-Flow Graph (program’s structure)
* System calls Sequences,
* Synchronization Mechanisms,
* Array bounds,
* User-defined invariants, and
* I/O behaviors

## Construction of Petri net based models for C programs

https://cse.iitkgp.ac.in/~chitta/pubs/rep/thesisKulwant.pdf

Compilarir eru tíverri oftani torførir at arbeiða við orsaka av teimum optimizeringum sum teir lova. Teir skullu nemlig vátta at forriti áðrenn optimering er behaviour equivalent við tí ið kom út úr optimerings processini. Hetta er torfort, men opinbart eru Petri-Net the shit at samman líkna hesi tingini (veit ikki hví).

Í staðin fyri at nýta Petri net, so nýtur hendan thesis PRES+, ið stendur fyri Petri net based Representation of Embedded Systems. PRES+ er ein extension til Petri-Nets, ið loyvur input-places, output-places, variablar, expressional assignments, og guards.

Workflow:

Avmarkingar:
* Only integer variables and arrays must be used.
* Every `scanf()` and `printf()` call must read and write exactly one integer variable respectively and there must not be any other function calls.
* The program must contain exactly one function i.e. `main()` with `void` as its return type.
* The program must not contain any `goto` statements (although the intermediate cfg may contain such statements).

## Niðurstøða

So vítt eg dugdi at finna, so er eingin ið umsetur source-code til vanlig petri-net (við inhibitor arcs), uftan so, at har eru fúlar avmarkingar á (t.d perspektivir). Hóast har skal arbeiði til enn, so haldi eg at hetta er ein hóskandi verkætlan at fara í holt við. Serliga um vit kunnu gera ein "import" knøtt á TAPAAL ið loyvur at mann opnar C programmir sum um tað var PN.

Eg dugi eisini at ímynda mær at C kanska ikki er rætta málið at umseta, orsaka av hvussu RAM og bit fokusera málbólkurin er. Bara tað, at `malloc` er í málinum ger tað nokk so shit. Tí so verður ein noyddur at ganga út frá at alt kann liggja í RAM'inum. Kanska vit kundu valt eitt mál, ið tvingar upprudding, og harvið er lættari at umseta.

Aðrar avbjóðingar:
* Recursion: Hvussu gera vit ein fornuftigan "call-stack". Kanska onkur tól frá Murata kunnu hjálpa her.
* Strings: Hvussu representera vit streingir í einum PN? Kanska vit kundu nýtt onkran serligan hátt, ella brúkt colored PNs