Reject controllerSpec clauses other than controllable/safety with controlled_det
A controlled_det composition drives its determinisation purely from the controllable action set (TransitionSystemDispatcher.makeControlledDeterminisation reads goal.getControllableActions() and nothing else). The safety clause is also honoured, since its property is composed into the model beforehand via preProcessSafetyReqs. Every other controllerSpec clause (liveness, assumption, reachability, nonblocking, ...) is silently ignored, so a spec that includes one is misleading: it looks like it constrains the result but does not. Add a guard in CompositionExpression.buildAndSetGoal, fired only when isControlledDet, that aborts via Diagnostics.fatal when the goal definition carries any clause other than controllable or safety. Add ControlledDetGoalTest covering the rejection and confirming the guard does not over-fire on a controllable-only spec. Clean the silently-ignored clauses out of the existing controlled_det test fixtures (ControlledDeterminisationTests, Alphabet, and the FSP compose-all fixtures), keeping controllable and safety. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>