A2. Unrealizability #

Specification TrafficA1b (unrealizable core of size 2) on the playground: https://play.formal-methods.net/?check=SPECTRA&p=batboy-unmade-pope-velcro

Specification TrafficA2a (unrealizable core of size 1) on the playground: https://play.formal-methods.net/?check=SPECTRA&p=nail-trench-lemon-mouth

The Spectra project of this video project on GitHub: https://github.com/jringert/spectra-tutorial/tree/main/A2_unrealizability

Solution #

Specification TrafficA2b (unrealizable) on the playground: https://play.formal-methods.net/?check=SPECTRA&p=rising-fence-xbox-worst

Specification TrafficA2c (unrealizable) on the playground: https://play.formal-methods.net/?check=SPECTRA&p=jimmy-lash-crown-kilt

Specification TrafficA2d (unrealizable) on the playground: https://play.formal-methods.net/?check=SPECTRA&p=opium-buffed-draw-update

The Spectra project of this video project on GitHub: https://github.com/jringert/spectra-tutorial/tree/main/A2_unrealizability

Return to the Spectra Tutorial Overview