{"data":{"id":"10.4121/uuid:64cd25f4-4192-46d1-a951-9f99b452b48f","type":"dois","attributes":{"doi":"10.4121/uuid:64cd25f4-4192-46d1-a951-9f99b452b48f","prefix":"10.4121","suffix":"uuid:64cd25f4-4192-46d1-a951-9f99b452b48f","identifiers":[],"alternateIdentifiers":[],"creators":[{"name":"Hartmanns, Arnd","nameType":"Personal","givenName":"Arnd","familyName":"Hartmanns","nameIdentifiers":[{"nameIdentifier":"0000-0003-3268-8674","nameIdentifierScheme":"https://orcid.org/"}],"affiliation":[]}],"titles":[{"title":"A Statistical Model Checker for Nondeterminism and Rare Events (Artifact)"}],"publisher":"University of Twente","container":{},"publicationYear":2018,"subjects":[{"subject":"Statistics","subjectScheme":"Australian and New Zealand Standard Research Classification (ANZSRC), 2008","classificationCode":"0104"},{"subject":"FOS: Mathematics","schemeUri":"http://www.oecd.org/science/inno/38235147.pdf","subjectScheme":"Fields of Science and Technology (FOS)"},{"subject":"Business and Management","subjectScheme":"Australian and New Zealand Standard Research Classification (ANZSRC), 2008","classificationCode":"1503"},{"subject":"FOS: Economics and business","schemeUri":"http://www.oecd.org/science/inno/38235147.pdf","subjectScheme":"Fields of Science and Technology (FOS)"},{"subject":"formal verification"},{"subject":"rare event simulation"},{"subject":"statistical model checking"}],"contributors":[{"name":"Budde, C.E. (Carlos)","nameType":"Personal","affiliation":[],"contributorType":"Other","nameIdentifiers":[]},{"name":"D’Argenio, P.R. (Pedro)","nameType":"Personal","affiliation":[],"contributorType":"Other","nameIdentifiers":[]},{"name":"Sedwards, S. (Sean)","nameType":"Personal","affiliation":[],"contributorType":"Other","nameIdentifiers":[]},{"name":"University Of Twente, Formal Methods And Tools (FMT) Research Group","nameType":"Organizational","affiliation":[],"contributorType":"Other","nameIdentifiers":[]}],"dates":[{"date":"2018-03-01","dateType":"Issued"}],"language":"en","types":{"ris":"DATA","bibtex":"misc","citeproc":"dataset","schemaOrg":"Dataset","resourceType":"Dataset","resourceTypeGeneral":"Dataset"},"relatedIdentifiers":[{"relationType":"References","relatedIdentifier":"https://doi.org/10.1007/s10009-020-00563-2","relatedIdentifierType":"URL"},{"relationType":"References","relatedIdentifier":"https://doi.org/10.1007/978-3-319-89963-3_20","relatedIdentifierType":"URL"}],"relatedItems":[],"sizes":[],"formats":["media types: application/octet-stream, application/pdf, application/vnd.openxmlformats-officedocument.spreadsheetml.sheet, application/x-dosexec, application/zip, text/plain"],"version":"1","rightsList":[{"rights":"4TU General Terms of Use","rightsUri":"https://doi.org/10.4121/resource:terms_of_use"}],"descriptions":[{"description":"The Modest Toolset for quantitative modelling and verification includes the 'modes' statistical model checker. We present 'modes' in our TACAS 2018 tool paper titled \"A Statistical Model Checker for Nondeterminism and Rare Events\", with a particular focus on its capabilities in automated rare event simulation and in approximating optimal schedulers on nondeterministic models. In the paper, we present an experimental evaluation of the capabilities (in terms of the kinds of supported models and analyses), performance, and scalability (across multi-core and distributed setups). This artifact contains (1) the version of 'modes' and (2) the model files used for our experiments, (3) the raw experimental results, (4) summarising tabular views of those results (from which we derived the tables of results included in the paper), and (5) a Linux shell script to replicate a subset of the experiments. Since our complete experiments take several hours to complete and require powerful hardware and computer clusters, we have selected a subset for the replication script. It runs to completion within less than one hour on typical workstation hardware of today while still substantiating the main conclusions drawn in the paper.","descriptionType":"Abstract"}],"geoLocations":[],"fundingReferences":[],"xml":"PD94bWwgdmVyc2lvbj0iMS4wIiBlbmNvZGluZz0iVVRGLTgiPz4KPHJlc291cmNlIHhtbG5zPSJodHRwOi8vZGF0YWNpdGUub3JnL3NjaGVtYS9rZXJuZWwtNCIgeG1sbnM6eHNpPSJodHRwOi8vd3d3LnczLm9yZy8yMDAxL1hNTFNjaGVtYS1pbnN0YW5jZSIgeHNpOnNjaGVtYUxvY2F0aW9uPSJodHRwOi8vZGF0YWNpdGUub3JnL3NjaGVtYS9rZXJuZWwtNCBodHRwOi8vc2NoZW1hLmRhdGFjaXRlLm9yZy9tZXRhL2tlcm5lbC00LjQvbWV0YWRhdGEueHNkIj4KICA8aWRlbnRpZmllciBpZGVudGlmaWVyVHlwZT0iRE9JIj4xMC40MTIxL1VVSUQ6NjRDRDI1RjQtNDE5Mi00NkQxLUE5NTEtOUY5OUI0NTJCNDhGPC9pZGVudGlmaWVyPgogIDxjcmVhdG9ycz4KICAgIDxjcmVhdG9yPgogICAgICA8Y3JlYXRvck5hbWUgbmFtZVR5cGU9IlBlcnNvbmFsIj5Bcm5kIEhhcnRtYW5uczwvY3JlYXRvck5hbWU+CiAgICAgIDxnaXZlbk5hbWU+QXJuZDwvZ2l2ZW5OYW1lPgogICAgICA8ZmFtaWx5TmFtZT5IYXJ0bWFubnM8L2ZhbWlseU5hbWU+CiAgICAgIDxuYW1lSWRlbnRpZmllciBuYW1lSWRlbnRpZmllclNjaGVtZT0iaHR0cHM6Ly9vcmNpZC5vcmcvIj4wMDAwLTAwMDMtMzI2OC04Njc0PC9uYW1lSWRlbnRpZmllcj4KICAgIDwvY3JlYXRvcj4KICA8L2NyZWF0b3JzPgogIDx0aXRsZXM+CiAgICA8dGl0bGU+QSBTdGF0aXN0aWNhbCBNb2RlbCBDaGVja2VyIGZvciBOb25kZXRlcm1pbmlzbSBhbmQgUmFyZSBFdmVudHMgKEFydGlmYWN0KTwvdGl0bGU+CiAgPC90aXRsZXM+CiAgPHB1Ymxpc2hlcj5Vbml2ZXJzaXR5IG9mIFR3ZW50ZTwvcHVibGlzaGVyPgogIDxwdWJsaWNhdGlvblllYXI+MjAxODwvcHVibGljYXRpb25ZZWFyPgogIDxyZXNvdXJjZVR5cGUgcmVzb3VyY2VUeXBlR2VuZXJhbD0iRGF0YXNldCI+RGF0YXNldDwvcmVzb3VyY2VUeXBlPgogIDxzdWJqZWN0cz4KICAgIDxzdWJqZWN0IHN1YmplY3RTY2hlbWU9IkF1c3RyYWxpYW4gYW5kIE5ldyBaZWFsYW5kIFN0YW5kYXJkIFJlc2VhcmNoIENsYXNzaWZpY2F0aW9uIChBTlpTUkMpLCAyMDA4IiBjbGFzc2lmaWNhdGlvbkNvZGU9IjAxMDQiPlN0YXRpc3RpY3M8L3N1YmplY3Q+CiAgICA8c3ViamVjdCBzdWJqZWN0U2NoZW1lPSJBdXN0cmFsaWFuIGFuZCBOZXcgWmVhbGFuZCBTdGFuZGFyZCBSZXNlYXJjaCBDbGFzc2lmaWNhdGlvbiAoQU5aU1JDKSwgMjAwOCIgY2xhc3NpZmljYXRpb25Db2RlPSIxNTAzIj5CdXNpbmVzcyBhbmQgTWFuYWdlbWVudDwvc3ViamVjdD4KICAgIDxzdWJqZWN0PmZvcm1hbCB2ZXJpZmljYXRpb248L3N1YmplY3Q+CiAgICA8c3ViamVjdD5yYXJlIGV2ZW50IHNpbXVsYXRpb248L3N1YmplY3Q+CiAgICA8c3ViamVjdD5zdGF0aXN0aWNhbCBtb2RlbCBjaGVja2luZzwvc3ViamVjdD4KICA8L3N1YmplY3RzPgogIDxjb250cmlidXRvcnM+CiAgICA8Y29udHJpYnV0b3IgY29udHJpYnV0b3JUeXBlPSJPdGhlciI+CiAgICAgIDxjb250cmlidXRvck5hbWUgbmFtZVR5cGU9IlBlcnNvbmFsIj5CdWRkZSwgQy5FLiAoQ2FybG9zKTwvY29udHJpYnV0b3JOYW1lPgogICAgPC9jb250cmlidXRvcj4KICAgIDxjb250cmlidXRvciBjb250cmlidXRvclR5cGU9Ik90aGVyIj4KICAgICAgPGNvbnRyaWJ1dG9yTmFtZSBuYW1lVHlwZT0iUGVyc29uYWwiPkTigJlBcmdlbmlvLCBQLlIuIChQZWRybyk8L2NvbnRyaWJ1dG9yTmFtZT4KICAgIDwvY29udHJpYnV0b3I+CiAgICA8Y29udHJpYnV0b3IgY29udHJpYnV0b3JUeXBlPSJPdGhlciI+CiAgICAgIDxjb250cmlidXRvck5hbWUgbmFtZVR5cGU9IlBlcnNvbmFsIj5TZWR3YXJkcywgUy4gKFNlYW4pPC9jb250cmlidXRvck5hbWU+CiAgICA8L2NvbnRyaWJ1dG9yPgogICAgPGNvbnRyaWJ1dG9yIGNvbnRyaWJ1dG9yVHlwZT0iT3RoZXIiPgogICAgICA8Y29udHJpYnV0b3JOYW1lIG5hbWVUeXBlPSJPcmdhbml6YXRpb25hbCI+VW5pdmVyc2l0eSBvZiBUd2VudGUsIEZvcm1hbCBNZXRob2RzIGFuZCBUb29scyAoRk1UKSByZXNlYXJjaCBncm91cDwvY29udHJpYnV0b3JOYW1lPgogICAgPC9jb250cmlidXRvcj4KICA8L2NvbnRyaWJ1dG9ycz4KICA8ZGF0ZXM+CiAgICA8ZGF0ZSBkYXRlVHlwZT0iSXNzdWVkIj4yMDE4LTAzLTAxPC9kYXRlPgogIDwvZGF0ZXM+CiAgPHJlbGF0ZWRJZGVudGlmaWVycz4KICAgIDxyZWxhdGVkSWRlbnRpZmllciByZWxhdGVkSWRlbnRpZmllclR5cGU9IlVSTCIgcmVsYXRpb25UeXBlPSJSZWZlcmVuY2VzIj5odHRwczovL2RvaS5vcmcvMTAuMTAwNy9zMTAwMDktMDIwLTAwNTYzLTI8L3JlbGF0ZWRJZGVudGlmaWVyPgogICAgPHJlbGF0ZWRJZGVudGlmaWVyIHJlbGF0ZWRJZGVudGlmaWVyVHlwZT0iVVJMIiByZWxhdGlvblR5cGU9IlJlZmVyZW5jZXMiPmh0dHBzOi8vZG9pLm9yZy8xMC4xMDA3Lzk3OC0zLTMxOS04OTk2My0zXzIwPC9yZWxhdGVkSWRlbnRpZmllcj4KICA8L3JlbGF0ZWRJZGVudGlmaWVycz4KICA8Zm9ybWF0cz4KICAgIDxmb3JtYXQ+bWVkaWEgdHlwZXM6IGFwcGxpY2F0aW9uL29jdGV0LXN0cmVhbSwgYXBwbGljYXRpb24vcGRmLCBhcHBsaWNhdGlvbi92bmQub3BlbnhtbGZvcm1hdHMtb2ZmaWNlZG9jdW1lbnQuc3ByZWFkc2hlZXRtbC5zaGVldCwgYXBwbGljYXRpb24veC1kb3NleGVjLCBhcHBsaWNhdGlvbi96aXAsIHRleHQvcGxhaW48L2Zvcm1hdD4KICA8L2Zvcm1hdHM+CiAgPHZlcnNpb24+MTwvdmVyc2lvbj4KICA8cmlnaHRzTGlzdD4KICAgIDxyaWdodHMgcmlnaHRzVVJJPSJodHRwczovL2RvaS5vcmcvMTAuNDEyMS9yZXNvdXJjZTp0ZXJtc19vZl91c2UiPjRUVSBHZW5lcmFsIFRlcm1zIG9mIFVzZTwvcmlnaHRzPgogIDwvcmlnaHRzTGlzdD4KICA8ZGVzY3JpcHRpb25zPgogICAgPGRlc2NyaXB0aW9uIGRlc2NyaXB0aW9uVHlwZT0iQWJzdHJhY3QiPlRoZSBNb2Rlc3QgVG9vbHNldCBmb3IgcXVhbnRpdGF0aXZlIG1vZGVsbGluZyBhbmQgdmVyaWZpY2F0aW9uIGluY2x1ZGVzIHRoZSAnbW9kZXMnIHN0YXRpc3RpY2FsIG1vZGVsIGNoZWNrZXIuIFdlIHByZXNlbnQgJ21vZGVzJyBpbiBvdXIgVEFDQVMgMjAxOCB0b29sIHBhcGVyIHRpdGxlZCAiQSBTdGF0aXN0aWNhbCBNb2RlbCBDaGVja2VyIGZvciBOb25kZXRlcm1pbmlzbSBhbmQgUmFyZSBFdmVudHMiLCB3aXRoIGEgcGFydGljdWxhciBmb2N1cyBvbiBpdHMgY2FwYWJpbGl0aWVzIGluIGF1dG9tYXRlZCByYXJlIGV2ZW50IHNpbXVsYXRpb24gYW5kIGluIGFwcHJveGltYXRpbmcgb3B0aW1hbCBzY2hlZHVsZXJzIG9uIG5vbmRldGVybWluaXN0aWMgbW9kZWxzLiBJbiB0aGUgcGFwZXIsIHdlIHByZXNlbnQgYW4gZXhwZXJpbWVudGFsIGV2YWx1YXRpb24gb2YgdGhlIGNhcGFiaWxpdGllcyAoaW4gdGVybXMgb2YgdGhlIGtpbmRzIG9mIHN1cHBvcnRlZCBtb2RlbHMgYW5kIGFuYWx5c2VzKSwgcGVyZm9ybWFuY2UsIGFuZCBzY2FsYWJpbGl0eSAoYWNyb3NzIG11bHRpLWNvcmUgYW5kIGRpc3RyaWJ1dGVkIHNldHVwcykuIFRoaXMgYXJ0aWZhY3QgY29udGFpbnMgKDEpIHRoZSB2ZXJzaW9uIG9mICdtb2RlcycgYW5kICgyKSB0aGUgbW9kZWwgZmlsZXMgdXNlZCBmb3Igb3VyIGV4cGVyaW1lbnRzLCAoMykgdGhlIHJhdyBleHBlcmltZW50YWwgcmVzdWx0cywgKDQpIHN1bW1hcmlzaW5nIHRhYnVsYXIgdmlld3Mgb2YgdGhvc2UgcmVzdWx0cyAoZnJvbSB3aGljaCB3ZSBkZXJpdmVkIHRoZSB0YWJsZXMgb2YgcmVzdWx0cyBpbmNsdWRlZCBpbiB0aGUgcGFwZXIpLCBhbmQgKDUpIGEgTGludXggc2hlbGwgc2NyaXB0IHRvIHJlcGxpY2F0ZSBhIHN1YnNldCBvZiB0aGUgZXhwZXJpbWVudHMuIFNpbmNlIG91ciBjb21wbGV0ZSBleHBlcmltZW50cyB0YWtlIHNldmVyYWwgaG91cnMgdG8gY29tcGxldGUgYW5kIHJlcXVpcmUgcG93ZXJmdWwgaGFyZHdhcmUgYW5kIGNvbXB1dGVyIGNsdXN0ZXJzLCB3ZSBoYXZlIHNlbGVjdGVkIGEgc3Vic2V0IGZvciB0aGUgcmVwbGljYXRpb24gc2NyaXB0LiBJdCBydW5zIHRvIGNvbXBsZXRpb24gd2l0aGluIGxlc3MgdGhhbiBvbmUgaG91ciBvbiB0eXBpY2FsIHdvcmtzdGF0aW9uIGhhcmR3YXJlIG9mIHRvZGF5IHdoaWxlIHN0aWxsIHN1YnN0YW50aWF0aW5nIHRoZSBtYWluIGNvbmNsdXNpb25zIGRyYXduIGluIHRoZSBwYXBlci48L2Rlc2NyaXB0aW9uPgogIDwvZGVzY3JpcHRpb25zPgo8L3Jlc291cmNlPg==","url":"https://data.4tu.nl/articles/_/12697496/1","contentUrl":null,"metadataVersion":15,"schemaVersion":"http://datacite.org/schema/kernel-4","source":"mds","isActive":true,"state":"findable","reason":null,"viewCount":1,"viewsOverTime":[{"yearMonth":"2025-08","total":1}],"downloadCount":0,"downloadsOverTime":[{"yearMonth":"2025-08","total":0}],"referenceCount":2,"citationCount":0,"citationsOverTime":[],"partCount":0,"partOfCount":0,"versionCount":0,"versionOfCount":0,"created":"2018-03-01T08:58:54.000Z","registered":"2018-03-01T08:58:55.000Z","published":"2018","updated":"2021-10-31T16:38:16.000Z"},"relationships":{"client":{"data":{"id":"delft.data4tu","type":"clients"}},"provider":{"data":{"id":"scpr","type":"providers"}},"media":{"data":{"id":"10.4121/uuid:64cd25f4-4192-46d1-a951-9f99b452b48f","type":"media"}},"references":{"data":[{"id":"10.1007/978-3-319-89963-3_20","type":"dois"},{"id":"10.1007/s10009-020-00563-2","type":"dois"}]},"citations":{"data":[]},"parts":{"data":[]},"partOf":{"data":[]},"versions":{"data":[]},"versionOf":{"data":[]}}}}