mc-imperial / spirv-control-flow

Formal modelling of SPIR-V control flow using Alloy
Apache License 2.0
2 stars 0 forks source link

Reachability for Reducibility #40

Open vili-1 opened 2 years ago

vili-1 commented 2 years ago

After implementing the reducibility in our model, this example from CTS does not satisfy the reducibility predicate. The exact reason is that block 20 is not reachable from entry. Reachability from entry is crucial for establishing well-formed flows.

What do you think?

s253

253.zip