<commit_before><?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
<meta name="generator" content="http://www.nongnu.org/elyxer/"/>
<meta name="create-date" content="2014-07-18"/>
 <LINK href="../style.css" rel="stylesheet" type="text/css">
<title>Cloud based distributed TLC</title>
</head>
<body>
<div id="globalWrapper">
<h1 class="title">
Cloud based distributed TLC
</h1>
<h1 class="Section">
<a class="toc" name="toc-Section-1">1</a> Motivation
</h1>
<ul>
<li>
Move long running model checking off local machine into the cloud (Short running models not ideal because instance spin-up time is approximately five minutes)
</li>
<li>
Maximize cloud instance resource utilization by providing fine-tuned TLC parameter pre-sets optimized for the given cloud instance type
</li>
<li>
Minimizes costs by terminating cloud instances immediately after TLC model checking has ended<ul>
<li>
Unless email delivery of model checking result fails (n this case the machine remains running for the user to pick up the result manually)
</li>
<li>
User then has to terminate the instance manually!
</li>

</ul>

</li>

</ul>
<h1 class="Section">
<a class="toc" name="toc-Section-2">2</a> Warning
</h1>
<div class="Unindented">
Using cloud based TLC launches compute instances at your cloud provider which may incur costs. While the cloud based distributed TLC tries to minimize costs by terminating instances as soon as possible, do not rely on it. Always check if cloud instances have been correctly terminated.
</div>
<h1 class="Section">
<a class="toc" name="toc-Section-3">3</a> Limitation
</h1>
<ul>
<li>
Only supports a single cloud provider (<a class="URL" href="http://aws.amazon.com/ec2/">Amazon EC2</a>) as of now
</li>
<li>
Runs TLC in non-distributed mode on a single cloud instance only as of now
</li>
<li>
Only a single instance type (<a class="URL" href="http://en.wikipedia.org/wiki/Amazon_Elastic_Compute_Cloud#Instance_types">m4.2xlarge</a>) supported as of now 
</li>
<li>
Cloud based distributed TLC cannot recover from a checkpoint
</li>

</ul>
<h1 class="Section">
<a class="toc" name="toc-Section-4">4</a> Usage
</h1>
<ol>
<li>
Set <a class="URL" href="http://docs.aws.amazon.com/general/latest/gr/managing-aws-access-keys.html">AWS access key and secret</a> as <a class="URL" href="http://en.wikipedia.org/wiki/Environment_variable">environment variables</a> prior to launching the Toolbox. See the example with dummy keys below.<ol>
<li>
<div class="listing">
<pre class="listing">export AWS_ACCESS_KEY_ID=AKIA7D89HCLJKHZASD7F
export AWS_SECRET_ACCESS_KEY=6FDASAIG7DAS976TYDKHCGQAS5D\FA77
</pre>
</div>

</li>

</ol>

</li>
<li>
Create a specification and a model
</li>
<li>
Open your model in the model editor <div class="float">
<a class="Label" name="Figure-1"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="ModelEditorA.png" alt="figure ModelEditorA.png" style="max-width: 800px; max-height: 600px;"/>
<div class="caption">
Figure 1 Model Editor
</div>

</div>

</div>

</li>
<li>
Expand the &ldquo;How to run&rdquo; section of the &ldquo;Model Overview&rdquo; page <div class="float">
<a class="Label" name="Figure-2"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="ModelEditorB.png" alt="figure ModelEditorB.png" style="max-width: 800px; max-height: 600px;"/>
<div class="caption">
Figure 2 How to run section
</div>

</div>

</div>

</li>
<li>
Select &ldquo;aws-ec2&rdquo; from the &ldquo;Run in distributed mode&rdquo; drop down <div class="float">
<a class="Label" name="Figure-3"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="ModelEditorC.png" alt="figure ModelEditorC.png" style="max-width: 800px; max-height: 600px;"/>
<div class="caption">
Figure 3 Select your cloud provider
</div>

</div>

</div>

</li>
<li>
Enter an email address into &ldquo;Result mailto address&rdquo; at which you want to receive the model checking result <div class="float">
<a class="Label" name="Figure-4"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="ModelEditorD.png" alt="figure ModelEditorD.png" style="max-width: 800px; max-height: 600px;"/>
<div class="caption">
Figure 4 Enter your email address
</div>

</div>

</div>

</li>
<li>
Click &ldquo;Run TLC&rdquo; to start model checking in the cloud and wait for the start-up to finish (it takes approximately five minutes to set-up the cloud instance)<ol>
<li>
The Toolbox switches to the &ldquo;Model checking results&rdquo; page and opens a progress dialog indicating the state of cloud instance provisioning <div class="float">
<a class="Label" name="Figure-5"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="ProgressBar.png" alt="figure ProgressBar.png" style="max-width: 800px; max-height: 600px;"/>
<div class="caption">
Figure 5 Progress Dialog
</div>

</div>

</div>

</li>
<li>
After provisioning the cloud instance, the Toolbox prompts the user to open a website in a browser. <div class="float">
<a class="Label" name="Figure-6"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="ProgressBarFinal.png" alt="figure ProgressBarFinal.png" style="max-width: 800px; max-height: 600px;"/>
<div class="caption">
Figure 6 Progress Dialog Final
</div>

</div>

</div>
 This website is hosted on the cloud instance and shows the TLC process output as well as runtime statistics similar to Toolbox stats <div class="float">
<a class="Label" name="Figure-7"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="MCoutInBrowser.png" alt="figure MCoutInBrowser.png" style="max-width: 800px; max-height: 600px;"/>
<div class="caption">
Figure 7 TLC runtime statistics in your browser
</div>

</div>

</div>

</li>

</ol>

</li>
<li>
Walk out and enjoy the weekend while TLC is busy checking 
</li>
<li>
On Monday expect to find an email in your inbox <div class="float">
<a class="Label" name="Figure-8"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="EMailResult.png" alt="figure EMailResult.png" style="max-width: 800px; max-height: 600px;"/>
<div class="caption">
Figure 8 Email Result
</div>

</div>

</div>

</li>
<li>
Save MC.out file somewhere to disc
</li>
<li>
Switch back to the Toolbox and open the model editor
</li>
<li>
Open the &ldquo;Model Checking Results&rdquo; page <div class="float">
<a class="Label" name="Figure-9"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="LoadResultIntoToolbox.png" alt="figure LoadResultIntoToolbox.png" style="max-width: 800px; max-height: 600px;"/>
<div class="caption">
Figure 9 Load result into Toolbox
</div>

</div>

</div>
 
</li>
<li>
<a class="Label" name="enu:Import-the-MC.out"> </a>Import the MC.out from disc <div class="float">
<a class="Label" name="Figure-10"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="LoadIntoResultPageB.png" alt="figure LoadIntoResultPageB.png" style="max-width: 1073px; max-height: 791px;"/>
<div class="caption">
Figure 10 Load into results page
</div>

</div>

</div>

</li>
<li>
Voilá <div class="float">
<a class="Label" name="Figure-11"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="FinalResultLoaded.png" alt="figure FinalResultLoaded.png" style="max-width: 1074px; max-height: 789px;"/>
<div class="caption">
Figure 11 Final result loaded
</div>

</div>

</div>

</li>

</ol>
<h1 class="Section">
<a class="toc" name="toc-Section-5">5</a> Common problems
</h1>
<ul>
<li>
The Toolbox fails to start the cloud instance<ul>
<li>
Re-check your credentials
</li>
<li>
If your credentials are correct, please turn on debug logging (!!!INSTRUCTIONS here!!!) and send us the output. You might have encountered a bug in cloud based distributed TLC.
</li>

</ul>

</li>
<li>
The runtime statistics (web browser) indicate that TLC has finished model checking, but no result is sent via email.<ul>
<li>
Check your email spam folder if the model checking result has incorrectly been classified as spam
</li>
<li>
Another reason why mail delivery might fail are too strict spam countermessures at the mail server level. You might want to try to use a different email address (domain part) in the future.<ul>
<li>
Copy &amp; paste the MC.out content from the browser window into a plain text file and load it from there (see <a class="Reference" href="#enu:Import-the-MC.out">4↑</a>)
</li>

</ul>

</li>

</ul>

</li>

</ul>

</div>
</body>
</html>
<commit_msg>Link to the vimeo introductory screencast.<commit_after><?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8"/>
<meta name="generator" content="http://www.nongnu.org/elyxer/"/>
<meta name="create-date" content="2014-07-18"/>
 <LINK href="../style.css" rel="stylesheet" type="text/css">
<title>Cloud based distributed TLC</title>
</head>
<body>
<div id="globalWrapper">
<h1 class="title">
Cloud based distributed TLC
</h1>
<h1 class="Section">
<a class="toc" name="toc-Section-1">1</a> Motivation
</h1>
<ul>
<li>
Move long running model checking off local machine into the cloud (Short running models not ideal because instance spin-up time is approximately five minutes)
</li>
<li>
Maximize cloud instance resource utilization by providing fine-tuned TLC parameter pre-sets optimized for the given cloud instance type
</li>
<li>
Minimizes costs by terminating cloud instances immediately after TLC model checking has ended<ul>
<li>
Unless email delivery of model checking result fails (n this case the machine remains running for the user to pick up the result manually)
</li>
<li>
User then has to terminate the instance manually!
</li>

</ul>

</li>

</ul>
<h1 class="Section">
<a class="toc" name="toc-Section-2">2</a> Warning
</h1>
<div class="Unindented">
Using cloud based TLC launches compute instances at your cloud provider which may incur costs. While the cloud based distributed TLC tries to minimize costs by terminating instances as soon as possible, do not rely on it. Always check if cloud instances have been correctly terminated.
</div>
<h1 class="Section">
<a class="toc" name="toc-Section-3">3</a> Limitation
</h1>
<ul>
<li>
Only supports a single cloud provider (<a class="URL" href="http://aws.amazon.com/ec2/">Amazon EC2</a>) as of now
</li>
<li>
Runs TLC in non-distributed mode on a single cloud instance only as of now
</li>
<li>
Only a single instance type (<a class="URL" href="http://en.wikipedia.org/wiki/Amazon_Elastic_Compute_Cloud#Instance_types">m4.2xlarge</a>) supported as of now 
</li>
<li>
Cloud based distributed TLC cannot recover from a checkpoint
</li>

</ul>
<h1 class="Section">
<a class="toc" name="toc-Section-4">4</a> Usage
</h1>

<div align="left">
<div align="center" style="width:500px;height:45px;border:1px solid #000;">
<em>Additionally to the instructions below, you can <a href="https://vimeo.com/126244715">watch a eight minutes introductory video</a> online</em>.
</div>
</div>

<ol>
<li>
Set <a class="URL" href="http://docs.aws.amazon.com/general/latest/gr/managing-aws-access-keys.html">AWS access key and secret</a> as <a class="URL" href="http://en.wikipedia.org/wiki/Environment_variable">environment variables</a> prior to launching the Toolbox. See the example with dummy keys below.<ol>
<li>
<div class="listing">
<pre class="listing">export AWS_ACCESS_KEY_ID=AKIA7D89HCLJKHZASD7F
export AWS_SECRET_ACCESS_KEY=6FDASAIG7DAS976TYDKHCGQAS5D\FA77
</pre>
</div>

</li>

</ol>

</li>
<li>
Create a specification and a model
</li>
<li>
Open your model in the model editor <div class="float">
<a class="Label" name="Figure-1"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="ModelEditorA.png" alt="figure ModelEditorA.png" style="max-width: 800px; max-height: 600px;"/>
<div class="caption">
Figure 1 Model Editor
</div>

</div>

</div>

</li>
<li>
Expand the &ldquo;How to run&rdquo; section of the &ldquo;Model Overview&rdquo; page <div class="float">
<a class="Label" name="Figure-2"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="ModelEditorB.png" alt="figure ModelEditorB.png" style="max-width: 800px; max-height: 600px;"/>
<div class="caption">
Figure 2 How to run section
</div>

</div>

</div>

</li>
<li>
Select &ldquo;aws-ec2&rdquo; from the &ldquo;Run in distributed mode&rdquo; drop down <div class="float">
<a class="Label" name="Figure-3"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="ModelEditorC.png" alt="figure ModelEditorC.png" style="max-width: 800px; max-height: 600px;"/>
<div class="caption">
Figure 3 Select your cloud provider
</div>

</div>

</div>

</li>
<li>
Enter an email address into &ldquo;Result mailto address&rdquo; at which you want to receive the model checking result <div class="float">
<a class="Label" name="Figure-4"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="ModelEditorD.png" alt="figure ModelEditorD.png" style="max-width: 800px; max-height: 600px;"/>
<div class="caption">
Figure 4 Enter your email address
</div>

</div>

</div>

</li>
<li>
Click &ldquo;Run TLC&rdquo; to start model checking in the cloud and wait for the start-up to finish (it takes approximately five minutes to set-up the cloud instance)<ol>
<li>
The Toolbox switches to the &ldquo;Model checking results&rdquo; page and opens a progress dialog indicating the state of cloud instance provisioning <div class="float">
<a class="Label" name="Figure-5"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="ProgressBar.png" alt="figure ProgressBar.png" style="max-width: 800px; max-height: 600px;"/>
<div class="caption">
Figure 5 Progress Dialog
</div>

</div>

</div>

</li>
<li>
After provisioning the cloud instance, the Toolbox prompts the user to open a website in a browser. <div class="float">
<a class="Label" name="Figure-6"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="ProgressBarFinal.png" alt="figure ProgressBarFinal.png" style="max-width: 800px; max-height: 600px;"/>
<div class="caption">
Figure 6 Progress Dialog Final
</div>

</div>

</div>
 This website is hosted on the cloud instance and shows the TLC process output as well as runtime statistics similar to Toolbox stats <div class="float">
<a class="Label" name="Figure-7"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="MCoutInBrowser.png" alt="figure MCoutInBrowser.png" style="max-width: 800px; max-height: 600px;"/>
<div class="caption">
Figure 7 TLC runtime statistics in your browser
</div>

</div>

</div>

</li>

</ol>

</li>
<li>
Walk out and enjoy the weekend while TLC is busy checking 
</li>
<li>
On Monday expect to find an email in your inbox <div class="float">
<a class="Label" name="Figure-8"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="EMailResult.png" alt="figure EMailResult.png" style="max-width: 800px; max-height: 600px;"/>
<div class="caption">
Figure 8 Email Result
</div>

</div>

</div>

</li>
<li>
Save MC.out file somewhere to disc
</li>
<li>
Switch back to the Toolbox and open the model editor
</li>
<li>
Open the &ldquo;Model Checking Results&rdquo; page <div class="float">
<a class="Label" name="Figure-9"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="LoadResultIntoToolbox.png" alt="figure LoadResultIntoToolbox.png" style="max-width: 800px; max-height: 600px;"/>
<div class="caption">
Figure 9 Load result into Toolbox
</div>

</div>

</div>
 
</li>
<li>
<a class="Label" name="enu:Import-the-MC.out"> </a>Import the MC.out from disc <div class="float">
<a class="Label" name="Figure-10"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="LoadIntoResultPageB.png" alt="figure LoadIntoResultPageB.png" style="max-width: 1073px; max-height: 791px;"/>
<div class="caption">
Figure 10 Load into results page
</div>

</div>

</div>

</li>
<li>
Voilá <div class="float">
<a class="Label" name="Figure-11"> </a><div class="figure" style="max-width: 100%;">
<img class="figure" src="FinalResultLoaded.png" alt="figure FinalResultLoaded.png" style="max-width: 1074px; max-height: 789px;"/>
<div class="caption">
Figure 11 Final result loaded
</div>

</div>

</div>

</li>

</ol>
<h1 class="Section">
<a class="toc" name="toc-Section-5">5</a> Common problems
</h1>
<ul>
<li>
The Toolbox fails to start the cloud instance<ul>
<li>
Re-check your credentials
</li>
<li>
If your credentials are correct, please turn on debug logging (!!!INSTRUCTIONS here!!!) and send us the output. You might have encountered a bug in cloud based distributed TLC.
</li>

</ul>

</li>
<li>
The runtime statistics (web browser) indicate that TLC has finished model checking, but no result is sent via email.<ul>
<li>
Check your email spam folder if the model checking result has incorrectly been classified as spam
</li>
<li>
Another reason why mail delivery might fail are too strict spam countermessures at the mail server level. You might want to try to use a different email address (domain part) in the future.<ul>
<li>
Copy &amp; paste the MC.out content from the browser window into a plain text file and load it from there (see <a class="Reference" href="#enu:Import-the-MC.out">4↑</a>)
</li>

</ul>

</li>

</ul>

</li>

</ul>

</div>
</body>
</html>

{'fraction_non_alphanumeric': 0.1626221772834513, 'fraction_numerical': 0.022357038534996067, 'mean_word_length': 5.353675945753033, 'pattern_counts': {'":': 0, '<': 493, '<?xml version=': 2, '>': 493, 'https://': 1, 'lorem ipsum': 0, 'www.': 6, 'xml': 6}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6955527', 'n_tokens_mistral': 6417, 'n_tokens_neox': 5934, 'n_words': 2067}