Finding Winning Strategies based on Discrete Abstractions

Computing a discrete abstraction is simple once a PAHS has been defined.

With the discrete game computed and corresponding specification a winning strategy can be computed using UppAal.

Finding a winning strategy
%Get the pahs
pahs=demopahs2();

%Compute the discrete abstraction
dgabs=finddiscgame(pahs);

%Get the requirement and convert them to a specification
req=demoreq2();
spec=req2spec(pahs,req);

%Try to find a winning strategy using UppAal
[win,sol]=finddgsol(dgabs,spec);

%Check if a winning strategy was found
if(win)
   disp('Winning')
else
   disp('Loosing')
end