Please choose your input example.
You may use an example in our test set or design your own example.
The gate controller of a railroad crossing has a delay of a seconds;
that is, the gate starts closing a seconds after a train signals its
HyTech computes the safe values of a such that the gate is fully
closed whenever the train is within 10 meters of the gate.
Fischer's shared-variables protocol relies on timing to ensure mutual
exclusion between two processes.
HyTech computes the safe values for the duration a of shared-memory
accesses and the duration b of explicit delays, assuming that all
durations are measured by drifting local clocks.