vis-ar-formalization Formalization of the (VIS, AR) Specification Framework for Both Transactional and Non-Transactional Consistency Models alloy tlaplus