class Post {

	string title;
	string body;
	
	//@ invariant true;
	//@ initial true;
	void Post(string t, string c) {
		title = t;
		body = c;
	}

	//@ requires true;
	//@ ensures true;
	string readPost() {
		title ++ " - " ++ body;
	}
}

class Blog {

	Post post;
	int no_views;
	
	boolean is_public;
	
	//@ invariant true;
	//@ initial !is_public && post == null;
	void Blog() {
		is_public = true;
	}
	
	//@ requires !is_public && post == null && p != null;
	//@ ensures !is_public && post != null;
	void newPost(string title, string body) {
		post = new Post(title, body);
	}
	
	//@ requires !is_public && post != null;
	//@ ensures !is_public && post == null;
	void deletePost() {
		post = null;
	}
	
	//@ requires true;
	//@ ensures |result| -> post != null;
	boolean hasPost() {
		post != null;
	}
	
	//@ requires true;
	//@ ensures |result| -> is_public;
	boolean postIsPublic() {
		post != null;
	}
	
	//@ requires is_public && post != null;
	//@ ensures is_public && post != null;
	sync Post viewPost() {
		no_views = no_views + 1;
		printStr("This post has ");
		printInt(no_views);
		printStr(" visualizations.");
		post;
	}
	
	//@ requires !is_public && post != null;
	//@ ensures is_public && post != null;
	void publishPost() {
		is_public = false;
	}
}

class Viewer {

	Blog blog;
	Post post;	
	boolean session;
	
	//@ invariant true;
	//@ requires b.postIsPublic();
	//@ initial post == null && blog != null && session;
	void Viewer(Blog b) {
		blog = b;
		session = true;
	}
	
	//@ requires post == null && blog != null && session;
	//@ ensures (blog != null && session) && (|result| -> post != null);
	boolean requestPost() {
		if(blog.postIsPublic()) {
			post = blog.viewPost();
			true;
		} else {
			printStr("Access denied");
			false;
		}
	}
	
	//@ requires post != null && blog != null && session;
	//@ ensures post != null && blog != null && session;
	void readPost() {
		printStr(post.viewPost());
	}
	
	//@ requires blog != null && session;
	//@ ensures blog != null && !session;
	void endSession() {
		session = false;
	}
}

unrestricted class Main {
	
	//@ invariant true;
	//@ initial true;
	void Main() {
		Blog blog; Blog = new Blog();
		
		blog.newPost("Sodales", "Lorem ipsum dolor sit amet");
		blog.submitPost();
		
		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();
		}
	}
}