A Three by Three Puzzle

Solve the 3x3 puzzle using Design Verifier

This is a Simulink Model of a 3x3 puzzle. This is a children's game where we could slide the tiles and make the numbers in the consecutive order. The moves are hardcoded. Based on where the blank tile is a certain set of moves are possible. This is modeled as an exchange of tiles. This has not been made as generic. A Matlab code could perhaps make it easier to model a generic N x N square. Simulink Design Verifier solves the tiles problem.