Selected Topics in Design & Verification

Model Checking and Synthesis with SMT

1. Verifying system against LTL spec → checking emptiness for NBW → finding bad lassos in run graph → checking existence of ranking functions → SMT model checking
2. Synthesizing system from LTL spec → using UF to represent transition relation and iterating through the possible numbers of states ($\le ~|B|^{|B|}$) → SMT model checking
3. In 1989, Pnueli and Rosner solved the LTL synthesis problem (2EXPTIME-complete): LTL $\phi$ → NBW (~ $2^{|\phi|}$) → DPW (~ $2^{|\phi|^{|\phi|}}$) → solve the game (~ $2^{|\phi|^{|\phi|}}$)

(DPW: deterministic parity word automata; NBW: nondeterministic Buchi word automata)

Downgrade from PHP 7 to PHP 5.6 on Ubuntu

http://askubuntu.com/questions/109404/how-do-i-install-different-upgrade-or-downgrade-php-version-in-still-supported

http://askubuntu.com/questions/761713/how-can-i-downgrade-from-php-7-to-php-5-6-on-ubuntu-16-04

Remove files from git history

http://stevelorek.com/how-to-shrink-a-git-repository.html

Model checking safety properties

Regular model checking

Regular Model Checking Made Simple and Efficient

Regular Model Checking Without Transducers

Model Checking of Safety Properties

Finite presentations of infinite structures: Paper / Slide

DOA Tools and Mods

Documents

• Overview - http://bbs.3dmgame.com/thread-4791938-1-1.html
• Editing texture - https://www.ptt.cc/bbs/AC_In/M.1429727192.A.74B.html
• Using AutoLink - http://w11.zetaboards.com/SFxT_Mods/topic/11582418/1/

DLC Tools

• AutoLink Homepage
• Collection of DLC tools
• TMC to DLC convertor
• Texture editor

Mods

http://saafrats.deviantart.com/gallery/
http://www.loverslab.com/files/download/2627-doa5lr-h-lod-nude-mod-curvy-body/
http://www.loverslab.com/topic/56672-doa5lr-saafrats-h-lod-nude-mod-v10-curvy-body-mod/

Offline MySQL migration

http://serverfault.com/questions/659048/can-i-copy-the-entire-var-lib-mysql-folder-to-a-different-server-mysql-vs-mar

C# performance notes

• for v.s foreach
  1. for loops on List are a bit more than 2 times cheaper than foreach loops on List.
  2. Looping on Array is around 2 times cheaper than looping on List.
  3. As a consequence, looping on Array using for is 5 times cheaper than looping on List using foreach.
  4. LinkedList only allows foreach loops, as it would take quadratic time to loop a LinkedList through indices.
  5. Looping overheads: for < foreach; Array ~ List < ArrayList < LinkedList
• Everything stored in an ArrayList is an object. So be careful of the boxing/unboxing overhead.
• String concatenation overheads are negligible outside loops.