Uhm, are they that different, though? For instance, you can formally express at least a part of the "there should be a button that pulls in new data when click

Uhm, are they that different, though? For instance, you can formally express at least a part of the "there should be a button that pulls in new data when clicked" specification. In LTL, that would be something like something like: [] (buttonClicked -> <>newDataPulled) (Notice that I switched from actions (click, pull) to states (clicked, pulled), as LTL is a state-based logic.)