The artefact contains the codes related to the SDTMC encoder discussed in the paper which implements the model embedding which converts an ADTMC to an SDTMC. The ADTMC is modelled using mCRL2 first and then using the tools of mCRL2 converted first to an LPS followed by a conversion to a probabilistic LTS in the .aut format. This aut file is considered to be an input to the code (one of three), which has three variations, which generate: 1. Three machine-readable files for the PRISM model checker. 2. A human-readable PRISM code and 3. A human-readable PRISM SDTMC with a reward structure which can be edited. The outputs are then run on the PRISM model checker, a popular tool for model-checking SDTMCs. The specifications in APCTL and their embedded PCTL counterparts as mentioned in the paper are also provided in the repositories of each case study where the formulas are saved in the required PRISM input format to be verified. In a nutshell, to model check an ADTMC with respect to an APCTL property, model the system in mCRL2, generate its corresponding LPS and LTS, and use our code to transform it into an SDTMC and translate the APCTL formula to PCTL formula using the logic embedding discussed in the paper. The PCTL formula can then be verified on the SDTMC in PRISM. READ THE README FILE FOR DETAILED INSTRUCTIONS. The related publication to which this artefact is to appear at FORTE 2023 (43nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems). We will share the doi of the paper once we are assigned the same.