class Post {

	usage lin{Post; Q1} where
		Q1 = un{readPost; Q1};
	
	string title;
	string body;
	
	void Post(string t, string c) {
		title = t;
		body = c;
	}
	
	string readPost() {
		title ++ " - " ++ body;
	}
	
}

class Viewer {

	usage lin{Viewer; Q1} where
		Q1 = lin{endSession; end + requestPost; <Q2 + Q1>}
		Q2 = lin{endSession; end + readPost; Q2};
	
	Blog[Q3] blog;
	Post post;
	boolean session;
	
	void Viewer(Blog[Q3] b) {
		blog = b;
		session = true;
	}
	
	void endSession() {
		session = false;
	}
	
	void readPost() {
		printStr(post);
	}
	
	boolean requestPost() {
		if(blog.postIsPublic()) {
			post = blog.viewPost();
			true;
		} else {
			printStr("Access denied");
			false;
		}
	}
	
}

class Blog {

	usage lin{Blog; Q1} where
		Q1 = lin{postIsPublic; Q1 + hasPost; Q1 + newPost; Q2}
		Q2 = lin{publishPost; Q3 + postIsPublic; Q2 + hasPost; Q2 + deletePost; Q1}
		Q3 = un{viewPost; Q3 + postIsPublic; Q3 + hasPost; Q3};
	
	Post post;
	int no_views;
	boolean is_public;
	
	void Blog() {
		is_public = true;
	}
	
	void publishPost() {
		is_public = false;
	}
	
	sync Post[Q1] viewPost() {
		no_views = no_views + 1;
		printStr("This post has ");
		printInt(no_views);
		printStr(" visualizations.");
		post;
	}
	
	boolean postIsPublic() {
		post != null;
	}
	
	boolean hasPost() {
		post != null;
	}
	
	void deletePost() {
		post = null;
	}
	
	void newPost(string title, string body) {
		post = new Post(title, body);
	}
	
}

class Main {

	
	void Main() {
		Blog blog;
		Blog = new Blog();
		blog.newPost("Sodales", "Lorem ipsum dolor sit amet");
		blog;
		spawn {
			Viewer v1;
			v1 = new Viewer(blog);
			if(v1.requestPost()) {
				v1.readPost();
			}
			v1.endSession();
		}
		spawn {
			Viewer v2;
			v2 = new Viewer(blog);
			if(v2.requestPost()) {
				v2.readPost();
			}
			v2.endSession();
		}
		spawn {
			Viewer v3;
			v3 = new Viewer(blog);
			if(v3.requestPost()) {
				v3.readPost();
			}
			v3.endSession();
		}
	}
	
}