A1. Synthesize your first controller #

Specification TrafficL2 on the playground: https://play.formal-methods.net/?check=SPECTRA&p=snare-crouch-dole-chummy

Specification GridL2 on the playground (with large controller): https://play.formal-methods.net/?check=SPECTRA&p=turkey-same-letter-clunky

Spectra project on GitHub: https://github.com/jringert/spectra-tutorial/tree/main/A1_firstController

Solution #

Specification TrafficA1a on the playground: https://play.formal-methods.net/?check=SPECTRA&p=chomp-galore-deny-poach

Specification TrafficA1b on the playground (unrealizable): https://play.formal-methods.net/?check=SPECTRA&p=earwig-avenue-entire-curled

Spectra project on GitHub: https://github.com/jringert/spectra-tutorial/tree/main/A1_firstController

Return to the Spectra Tutorial Overview