{"id":1250,"date":"2021-10-01T10:53:24","date_gmt":"2021-10-01T02:53:24","guid":{"rendered":"http:\/\/lcs.ios.ac.cn\/fm2021\/?page_id=1250"},"modified":"2021-12-01T23:16:05","modified_gmt":"2021-12-01T15:16:05","slug":"momba-program-cst","status":"publish","type":"page","link":"http:\/\/lcs.ios.ac.cn\/fm2021\/momba-program-cst\/","title":{"rendered":"Momba Program"},"content":{"rendered":"<div class=\"fusion-fullwidth fullwidth-box fusion-builder-row-1 fusion-flex-container nonhundred-percent-fullwidth non-hundred-percent-height-scrolling\" style=\"background-color: rgba(255,255,255,0);background-position: center center;background-repeat: no-repeat;border-width: 0px 0px 0px 0px;border-color:#e2e2e2;border-style:solid;\" ><div class=\"fusion-builder-row fusion-row fusion-flex-align-items-flex-start\" style=\"max-width:1248px;margin-left: calc(-4% \/ 2 );margin-right: calc(-4% \/ 2 );\"><div class=\"fusion-layout-column fusion_builder_column fusion-builder-column-0 fusion_builder_column_1_1 1_1 fusion-flex-column\"><div class=\"fusion-column-wrapper fusion-flex-justify-content-flex-start fusion-content-layout-column\" style=\"background-position:left top;background-repeat:no-repeat;-webkit-background-size:cover;-moz-background-size:cover;-o-background-size:cover;background-size:cover;padding: 0px 0px 0px 0px;\"><div class=\"fusion-text fusion-text-1\"><h5 style=\"text-align: center;\"><span style=\"color: #ff0000;\">Beijing Time, UTC +8:00<\/span><\/h5>\n<div style=\"text-align: center; padding: 5pt 0pt 5pt 0pt; font-size: 12pt; margin: 4pt 0pt 4pt 0pt; background-color: #d4d4d4;\">Saturday, November 20th<\/div>\n<div style=\"font-size: 12pt; background-color: #d8e5e9; padding: 4pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt; color: #555;\"><span style=\"color: #666; font-weight: bold;\">16:00-17:00 <\/span>Session: Introduction and Setup [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/momba\/Momba-1.mp4\"><strong>video<\/strong><\/a><\/span>]<\/div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">16:00<\/td>\n<td>\n<div>Holger Hermanns, Maximilian K\u00f6hl<\/div>\n<div><strong>Introduction of Quantitative Modelling with Momba<\/strong><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">16:45<\/td>\n<td>\n<div>Holger Hermanns, Maximilian K\u00f6hl<\/div>\n<div><strong>Project Setup<\/strong><\/div>\n<div>\n<ul>\n<li>Getting started: We walk you through the process of setting up the provided project skeleton such that you can follow along. Please make sure to have\u00a0<a class=\"reference internal\" href=\"https:\/\/fm21.momba.dev\/preparation\/\"><span class=\"doc std std-doc\">prepared your system upfront<\/span><\/a>.<\/li>\n<li>Best practices: <strong>How to set up a Python project for reproducibility and easy collaboration? <\/strong>We will walk you through the provided project skeleton. You will learn how to manage dependencies in a way that enables reproducibility, prevents version conflicts, and makes collaboration easy. We will demonstrate how to use tools such as auto formatters and linters to ensure a consistent code style and how to use VS Code workspaces to unify the development environment across a project.<\/li>\n<li>Running example: We introduce the example you will be working with in more detail.<\/li>\n<li>Model construction: We introduce the theory behind Momba and the\u00a0<a class=\"reference external\" href=\"https:\/\/jani-spec.org\/\">JANI model format<\/a>.<\/li>\n<\/ul>\n<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<div style=\"font-size: 12pt; background-color: #eeeed9; padding: 3pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt;\"><span style=\"font-weight: bold; color: #555;\">17:00-17:30<\/span><span style=\"margin-left: 14pt; padding-left: 18pt; color: #555;\">Break<\/span><\/div>\n<div style=\"font-size: 12pt; background-color: #d8e5e9; padding: 4pt 5pt 3pt 5pt; margin: 3pt 0pt 1pt 0pt; color: #555;\"><span style=\"color: #666; font-weight: bold;\">17:30-19:30<\/span><span style=\"margin-left: 16pt;\">Session: Hands-on [<span style=\"color: #0000ff;\"><a style=\"color: #0000ff;\" href=\"http:\/\/lcs.ios.ac.cn\/fm2021\/recordings\/momba\/Momba-2.mp4\"><strong>video<\/strong><\/a><\/span>]<\/span><\/div>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">17:00<\/td>\n<td>\n<div>Holger Hermanns, Maximilian K\u00f6hl<\/div>\n<div><strong>Model Construction<\/strong><\/div>\n<div>\n<div>\n<p><strong>Model Construction: <\/strong><strong>How to\u00a0<em>construct<\/em>\u00a0a formal model with Momba?<\/strong><\/p>\n<p>We walk you through the API provided by Momba to programmatically construct JANI models. Afterwards, you will have the opportunity to develop a model on your own using the skeleton we provide.<\/p>\n<\/div>\n<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">18:25<\/td>\n<td>\n<div>Holger Hermanns, Maximilian K\u00f6hl<\/div>\n<div>\n<p><strong><strong>Model Exploration<\/strong><\/strong><\/p>\n<div>\n<p><strong>Model Validation: <\/strong><strong>How to\u00a0<em>validate<\/em>\u00a0a formal model with Momba?<\/strong><\/p>\n<p>We walk you through the state space exploration API provided by Momba. You will program an interactive visualization for your model.<\/p>\n<\/div>\n<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<table style=\"margin: 2pt 0pt 2pt 0pt;\">\n<tbody>\n<tr style=\"vertical-align: top;\">\n<td style=\"padding: 0pt 5pt 0pt 5pt; margin: 0pt 0pt 0pt 0pt;\">19:00<\/td>\n<td>\n<div>Holger Hermanns, Maximilian K\u00f6hl<\/div>\n<div>\n<p><strong><strong>Model Analysis<\/strong><\/strong><\/p>\n<p><strong>Model Analysis: <\/strong><strong>How to\u00a0<em>analyze<\/em>\u00a0a formal model with Momba?<\/strong><\/p>\n<p>We will briefly introduce quantitative model checking. We then walk you through the analysis API provided by Momba. Using this API, you will analyze properties of your model.<\/p>\n<\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<\/div><\/div><\/div><style type=\"text\/css\">.fusion-body .fusion-builder-column-0{width:100% !important;margin-top : 0px;margin-bottom : 20px;}.fusion-builder-column-0 > .fusion-column-wrapper {padding-top : 0px !important;padding-right : 0px !important;margin-right : 1.92%;padding-bottom : 0px !important;padding-left : 0px !important;margin-left : 1.92%;}@media only screen and (max-width:1024px) {.fusion-body .fusion-builder-column-0{width:100% !important;order : 0;}.fusion-builder-column-0 > .fusion-column-wrapper {margin-right : 1.92%;margin-left : 1.92%;}}@media only screen and (max-width:640px) {.fusion-body .fusion-builder-column-0{width:100% !important;order : 0;}.fusion-builder-column-0 > .fusion-column-wrapper {margin-right : 1.92%;margin-left : 1.92%;}}<\/style><\/div><style type=\"text\/css\">.fusion-body .fusion-flex-container.fusion-builder-row-1{ padding-top : 0px;margin-top : 0px;padding-right : 0px;padding-bottom : 0px;margin-bottom : 0px;padding-left : 0px;}<\/style><\/div>\n","protected":false},"excerpt":{"rendered":"","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":[],"_links":{"self":[{"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/pages\/1250"}],"collection":[{"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/comments?post=1250"}],"version-history":[{"count":15,"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/pages\/1250\/revisions"}],"predecessor-version":[{"id":1646,"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/pages\/1250\/revisions\/1646"}],"wp:attachment":[{"href":"http:\/\/lcs.ios.ac.cn\/fm2021\/wp-json\/wp\/v2\/media?parent=1250"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}