diff --git a/tutorials/online/maintext-FS-2.html b/tutorials/online/maintext-FS-2.html
index 6ed2f4b..ad3c941 100644
--- a/tutorials/online/maintext-FS-2.html
+++ b/tutorials/online/maintext-FS-2.html
@@ -15,7 +15,7 @@ File System Lesson I Walkthrough
In this lesson, we take a look at the Alloy interface
itself. We will walkthrough the basics of how to execute a
- command to check an Alloy model and how to interpret the
+ command, check an Alloy model for correctness and interpret the
results. We will continue to use our running sample model of a
File system, and execute the check statements to verify
@@ -33,9 +33,10 @@
Disclaimer
However, the basics of using the Alloy interface (what you
can tell Alloy to do, the terminology we use, and the kind
of information Alloy returns) remains constant. This walkthrough
- analyzes our File System example, and to show examples of what the resulting output and
- visualizations might look like. If you need additional help, or to report/clarify an
- inconsistency, feel free to contact us.
+ analyzes our File System example, and to show examples of what the
+ resulting output and visualizations might look like. If you need
+ additional help, or to report/clarify an inconsistency, feel free
+ to contact us.
@@ -52,8 +53,8 @@ Basics of using Alloy
-- Create a new model by pasting in our current model (shown to
- the right of this window), and save it as
+
- Create a new model by pasting in our current model (shown
+ to the right of this window), and save it as
'fileSystem.als'
- Select a command to execute by choosing one from the
'Execute' menu the menu bar. There will be
@@ -65,13 +66,14 @@
Basics of using Alloy
menu. You will be told "no counterexample found. Assertion may
be valid.", meaning that there are no counter examples
to the acyclic assertion within a scope of 5.
- Had there been solutions, you can click on message and display one such solution
- in a new visualizer window.
+ Had there been solutions, you can click on message and display one
+ such solution in a new visualizer window.
- Now let's check the second command the same way. Select
the second command ("check oneRoot for 5") from
the Execute menu, and execute it. There are no
solutions found for this one either.
-- Finally, check the third command the same way. There are n osolutions found for this one either.
+- Finally, check the third command the same way.
+ There are no solutions found for this one either.
@@ -80,9 +82,9 @@ Basics of using Alloy
In general, once you make a change to the model and want to see
its effect on a run or a check,
- just execute that command again. You do not need to click save first, since
- the Alloy Analyzer will always use the text editor's version rather than
- the version on disk.
+ just execute that command again. You do not need to click save first,
+ since the Alloy Analyzer will always use the text editor's version
+ rather than the version on disk.
We'll see an example of visualizing a solution next.
@@ -131,8 +133,8 @@ Visualizing a counterexample to an incorrect assertion
You can make the visualization more readable by customizing the
layout. You do this by clicking the "Theme" button from the toolbar. You
can adjust what relations and sets are shown, and the style of
- their presentation. Here is a cleaner customization by clicking on the "contents"
- relationship and setting its "Show as Arc" checkbox to false.
+ their presentation. Here is a cleaner customization by clicking
+ on the "contents" relationship and setting its "Show as Arc" checkbox to false.
@@ -161,7 +163,8 @@ Visualizing a counterexample to an incorrect assertion
- Or, with some minor customizations (by setting Dir to be blue parallelograms), we get the much more readable:
+ Or, with some minor customizations (by setting Dir to be blue
+ parallelograms), we get the much more readable:
