When reaching a goal MTSA allows to choose suboptimal successors
Example, in the LTS below once the robot has reached position (3,0) Controller is willing to go to (4,0) since after reaching a goal, she only restricts moves to winning states. However, a better strategy would be one in which she actually chooses her best successor according to the next goal.
const Zise = 4 range R = 0..Zise
const GoalRow_1 = 3 const GoalColumn_1 = 0
const GoalRow_2 = 1 const GoalColumn_2 = 1
const StartingRow = 0 const StartingColumn = 0
range DangerZoneRows = 0..4 range DangerZoneColumns = 3..4
set Gotos = {go[row:R][col:R]} set Arrivals = {{arrive}.[row:R][col:R]} set Detours = {{detour}.[row:R][col:R]} set ControllableActions = {Gotos} set UncontrollableActions = {Arrivals,Detours} set Alphabet = {ControllableActions, UncontrollableActions}
GRID = POS[StartingRow][StartingColumn], POS[row:R][col:R] = ( when (row<Zise) go[row+1][col]->GOING_TO[row+1][col] | when (col<Zise) go[row][col+1] ->GOING_TO[row][col+1] | when (row>0) go[row-1][col]->GOING_TO[row-1][col] | when (col>0) go[row][col-1]->GOING_TO[row][col-1]),
GOING_TO[row:R][col:R] = ( arrive[row][col]->POS[row][col] | when (row>0) detour[row-1][col]->POS[row-1][col] | when (row<Zise) detour[row+1][col]->POS[row+1][col] | when (col>0) detour[row][col-1]->POS[row][col-1] | when (col<Zise) detour[row][col+1]->POS[row][col+1] )+{Gotos,Arrivals,Detours}.
DRONE = ({Gotos}->ARRIVE), ARRIVE = ({Arrivals,Detours}->DRONE).
||ENV = (GRID || DRONE). fluent G[row:R][col:R] = <{arrive[row][col], detour[row][col]}, Alphabet{arrive[row][col], detour[row][col]}> fluent DangerZone[row:DangerZoneRows][col:DangerZoneColumns] = <{arrive[row][col], detour[row][col]}, Alphabet{arrive[row][col], detour[row][col]}>
set FailureSet = {detour[R][R]} fluent F_Failures = <FailureSet, Alphabet{FailureSet}>
assert G1 = G[GoalRow_1][GoalColumn_1] assert G2 = G[GoalRow_2][GoalColumn_2]
assert Failures = F_Failures constraint TESTF = Failures ||TEST = TESTF.
controllerSpec SPEC = { safety = {Safe} liveness = {G1,G2} failure = {Failures} controllable = {ControllableActions} }
assert TestFormula = (SafetyGoal && (Test_G1 && Test_G2)) assert Test_G1 = ([]<>(G1||Failures)) assert Test_G2 = ([]<>(G2||Failures)) assert SafetyGoal = ()
controller ||C = (ENV)~{SPEC}. ||ANIMAR = (C || ENV).