disco

layer exercise is
	class user is
		role: (unregistered, registered, bookshop_owner, admin);
		extend bookshop_owner by
				own_store: reference bookstore;
		end;
		is_super_admin:(no, yes);
	end;

	class bookstore is
		added: (no, yes);
	end;

	class book is
		state: (free, added, is_in_cart, sold);

		extend is_in_cart by
			in_cart: reference cart;
		end;
		extend sold by
			sold_user: reference user;
		end;

		in_store: reference bookstore;
	end;

	class cart is
	assigned: (no, yes);
		extend yes by
			owner: reference user;
		end;
	end;

	relation user_own_cart (user, cart) is 0..1: 0..1;

	--action for all user
	action user_browse(u: user) is
		when true do
	end;

	action user_seacrh(u: user) is
		when true do
	end;

	--user register / unregister from system

	action user_register(u: user; c: cart) is
		when u.role'unregistered and c.assigned'no do
			u.role -> registered()||
			c.assigned -> yes(owner := u)||
			user_own_cart(u,c)
			;
	end;

	action registered_user_unregister(u: user; c: cart) is
		when u.role'registered and user_own_cart(u,c) do
			u.role -> unregistered()||
			c.assigned -> no()||
			not user_own_cart(u,c)
			;
	end;

	action unregisterd_owner(u: user) is
		when (u.role'bookshop_owner) do
			u.role -> unregistered();
	end;

	action unregisterd_admin(u: user) is
		when (u.role'admin and not u.is_super_admin'yes) do
			u.role -> unregistered();
	end;

	--admin change role
	--change to unregistered
	action admin_unregisterd_registered_user(a: user; u: user; c: cart) is
		when (a.role'admin and u.role'registered and user_own_cart(u,c)) do
			u.role -> unregistered()||
			c.assigned -> no()||
			not user_own_cart(u,c)
			;
	end;

	action admin_unregisterd_owner(a: user; u: user) is
		when (a.role'admin and u.role'bookshop_owner ) do
			u.role -> unregistered();
	end;

	action admin_unregisterd_admin(a: user; u: user) is
		when (a.role'admin and u.role'admin and not u.is_super_admin'yes) do
			u.role -> unregistered();
	end;

	--change to registered
	action admin_change_admin_to_registered(a: user; u:user; c:cart) is
		when (a.role'admin and u.role'admin and c.assigned'no and not u.is_super_admin'yes) do
			u.role -> registered()||
			c.assigned -> yes(owner := u)||
			user_own_cart(u,c)
			;
	end;

	action admin_change_owner_to_registered(a: user; u: user; c:cart) is
		when (a.role'admin and u.role'bookshop_owner and c.assigned'no) do
			u.role -> registered()||
			c.assigned -> yes(owner := u)||
			user_own_cart(u,c)
			;
	end;

	--change to owner
	action admin_change_registered_to_owner(a: user; u: user; s: bookstore; c:cart) is
		when (a.role'admin and u.role'registered and user_own_cart(u,c) and s.added'yes) do
			u.role -> bookshop_owner(own_store := s)||
			c.assigned -> no()||
			not user_own_cart(u,c)
			;
	end;

	action admin_change_admin_to_owner(a: user; u:user; s: bookstore) is
		when (a.role'admin and u.role'admin and s.added'yes and not u.is_super_admin'yes) do
			u.role -> bookshop_owner(own_store := s);
	end;

	--change to admin
	action admin_change_registered_to_admin(a: user; u: user; c:cart) is
		when (a.role'admin and u.role'registered and user_own_cart(u,c)) do
			u.role -> admin()||
			c.assigned -> no()||
			not user_own_cart(u,c)
			;
	end;

	action admin_change_owner_to_admin(a: user; u: user) is
		when (a.role'admin and u.role'bookshop_owner) do
			u.role -> admin();
	end;

	--admin add store
	action admin_add_store(a: user; s: bookstore) is
		when (a.role'admin and s.added'no) do
			s.added -> yes();
	end;

	-- owner add/remove books
	action owner_add_book(o: user; s: bookstore; b: book) is
		when (o.role'bookshop_owner.own_store = s and b.state'free) do
			b.state -> added() ||
			b.in_store := s;
	end;

	action owner_remove_book(o: user; s: bookstore; b: book) is
		when (o.role'bookshop_owner.own_store = s and b.state'added and b.in_store = s) do
			b.state -> free() ||
			b.in_store := null;
	end;

	-- add/remove book from cart
	action user_add_book_to_cart(u: user; c: cart; b: book) is
		when u.role'registered and user_own_cart(u,c) and b.state'added do
			b.state -> is_in_cart(in_cart := c);
	end;

	action user_remove_book_from_cart(u: user; c: cart; b: book) is
		when u.role'registered and user_own_cart(u,c) and b.state'is_in_cart.in_cart = c do
			b.state -> added();
	end;

	action admin_remove_book_from_cart(u: user; c: cart; b: book) is
		when u.role'admin and b.state'is_in_cart.in_cart = c do
			b.state -> added();
	end;

	action user_pay_for_book_in_cart(u: user; c: cart; b: book) is
		when u.role'registered and user_own_cart(u,c) and b.state'is_in_cart.in_cart = c do
			b.state -> sold(sold_user := u);
	end;
end;