ftsrg / theta

Generic, modular and configurable formal verification framework supporting various formalisms and algorithms
http://theta.inf.mit.bme.hu/
Apache License 2.0
49 stars 43 forks source link

Urgent init location in XTA #245

Open szdan97 opened 1 year ago

szdan97 commented 1 year ago

Theta seems to handle urgent/commited initial locations incorrectly. Urgentness is generally handled by the transfunc through optionally applying a delay after all other modifications have been done, based on whether the target location configuration is urgent/commited or not. However, the initfunc always returns zero().up() independently of the type of the init locations.